Theorem pm3.24 926

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.)

Assertion

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

Proof of Theorem pm3.24

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  pm4.43  968  pssirr  3707  indifdir  3883  dfnul2  3917  dfnul3  3918  rabnc  3962  ralnralall  4080  imadif  5973  fiint  8237  kmlem16  8987  zorn2lem4  9321  nnunb  11288  indstr  11756  bwth  21213  lgsquadlem2  25106  frgrregord013  27253  difrab2  29339  ifeqeqx  29361  ballotlemodife  30559  sgn3da  30603  poimirlem30  33439  clsk1indlem4  38342  atnaiana  41090  plcofph  41111