[quchen]

Although intuitionistic logic does not have the axiom

    ------ (LEM)
    A ∨ ¬A

that is, the law of the exluded middle (LEM) can not be derived "from nothing" for all propositions, it is still an inconsistency if you can prove A ∧ ¬A to be true, since

                             ------ (Assumption)
                             A ∧ ¬A
    ------ (Assumption)      ------ (∧E2)
    A ∧ ¬A                     ¬A
    ------ (∧E1)             ------ (Definition of ¬)
        A                    A ⇒ ⊥
       ---------------------------- (⇒E)
                  ⊥
           --------------- (⇒I, discharge assumption)
              A ∧ ¬A ⇒ ⊥
           --------------- (Definition of ¬)
              ¬(A ∧ ¬A)

In other words, assuming A ∧ ¬A holds you can prove the false proposition ⊥ (from which you can prove anything).

(Note that the De Morgan's law ¬(A ∧ ¬A) ⇒ A ∨ ¬A does not hold without the LEM, so the above proof cannot be simplified in terms of it!)