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  4066  dfnul4  4298  dfnul3  4300  rabnc  4354  ralnralall  4478  imadif  6600  fiint  9277  fiintOLD  9278  kmlem16  10119  zorn2lem4  10452  nnunb  12438  indstr  12875  bwth  23297  lgsquadlem2  27292  frgrregord013  30324  difrab2  32427  ifeqeqx  32471  sgn3da  32759  ballotlemodife  34489  sbn1ALT  36846  poimirlem30  37644  clsk1indlem4  44033  atnaiana  46921  plcofph  46942