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  1024  pssirr  4053  dfnul4  4285  dfnul3  4287  rabnc  4341  ralnralall  4465  imadif  6565  fiint  9211  kmlem16  10054  zorn2lem4  10387  nnunb  12374  indstr  12811  bwth  23323  lgsquadlem2  27317  frgrregord013  30370  difrab2  32472  ifeqeqx  32517  sgn3da  32812  ballotlemodife  34506  sbn1ALT  36891  poimirlem30  37689  clsk1indlem4  44076  atnaiana  46953  plcofph  46974