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  4044  dfnul4  4276  dfnul3  4278  rabnc  4332  ralnralall  4454  imadif  6576  fiint  9230  kmlem16  10079  zorn2lem4  10412  nnunb  12424  indstr  12857  bwth  23385  lgsquadlem2  27358  frgrregord013  30480  difrab2  32582  ifeqeqx  32627  sgn3da  32922  ballotlemodife  34658  sbn1ALT  37181  poimirlem30  37985  clsk1indlem4  44489  atnaiana  47383  plcofph  47404