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  1023  pssirr  4126  dfnul4  4354  dfnul3  4356  dfnul2OLD  4357  dfnul3OLD  4358  noelOLD  4361  rabnc  4414  ralnralall  4538  imadif  6662  fiint  9394  fiintOLD  9395  kmlem16  10235  zorn2lem4  10568  nnunb  12549  indstr  12981  bwth  23439  lgsquadlem2  27443  frgrregord013  30427  difrab2  32526  ifeqeqx  32565  ballotlemodife  34462  sgn3da  34506  sbn1ALT  36824  poimirlem30  37610  clsk1indlem4  44006  atnaiana  46838  plcofph  46859