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 230	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 207  df-an 396

This theorem is referenced by:  pm4.43  1025  pssirr  4043  dfnul4  4275  dfnul3  4277  rabnc  4331  ralnralall  4453  imadif  6582  fiint  9237  kmlem16  10088  zorn2lem4  10421  nnunb  12433  indstr  12866  bwth  23375  lgsquadlem2  27344  frgrregord013  30465  difrab2  32567  ifeqeqx  32612  sgn3da  32907  ballotlemodife  34642  sbn1ALT  37165  poimirlem30  37971  clsk1indlem4  44471  atnaiana  47371  plcofph  47392