Theorem pm3.24 402

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	⊢ ¬ (𝜑 ∧ ¬ 𝜑)

Proof of Theorem pm3.24

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		iman 401	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 229	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  pm4.43  1019  pssirr  4031  indifdirOLD  4216  dfnul4  4255  dfnul3  4257  dfnul2OLD  4258  dfnul3OLD  4259  noelOLD  4262  rabnc  4318  ralnralall  4446  imadif  6502  fiint  9021  kmlem16  9852  zorn2lem4  10186  nnunb  12159  indstr  12585  bwth  22469  lgsquadlem2  26434  frgrregord013  28660  difrab2  30746  ifeqeqx  30786  ballotlemodife  32364  sgn3da  32408  sbn1ALT  34969  poimirlem30  35734  clsk1indlem4  41543  atnaiana  44305  plcofph  44326