Metamath Proof Explorer

Theorem pm3.24

Description: Law of noncontradiction. Theorem *3.24 of WhiteheadRussell p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993) (Proof shortened by Wolf Lammen, 24-Nov-2012)

Ref Expression
Assertion pm3.24 
|- -. ( ph /\ -. ph )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ph -> ph )
2 iman 
 |-  ( ( ph -> ph ) <-> -. ( ph /\ -. ph ) )
3 1 2 mpbi 
 |-  -. ( ph /\ -. ph )