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  4083  dfnul4  4315  dfnul3  4317  rabnc  4371  ralnralall  4495  imadif  6630  fiint  9348  fiintOLD  9349  kmlem16  10188  zorn2lem4  10521  nnunb  12505  indstr  12940  bwth  23364  lgsquadlem2  27361  frgrregord013  30342  difrab2  32445  ifeqeqx  32490  ballotlemodife  34459  sgn3da  34503  sbn1ALT  36818  poimirlem30  37616  clsk1indlem4  44019  atnaiana  46893  plcofph  46914