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  4057  dfnul4  4289  dfnul3  4291  rabnc  4345  ralnralall  4468  imadif  6584  fiint  9239  kmlem16  10088  zorn2lem4  10421  nnunb  12409  indstr  12841  bwth  23366  lgsquadlem2  27360  frgrregord013  30482  difrab2  32583  ifeqeqx  32628  sgn3da  32925  ballotlemodife  34675  sbn1ALT  37100  poimirlem30  37895  clsk1indlem4  44394  atnaiana  47277  plcofph  47298