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 229	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 206  df-an 396

This theorem is referenced by:  pm4.43  1021  pssirr  4096  indifdirOLD  4281  dfnul4  4320  dfnul3  4322  dfnul2OLD  4323  dfnul3OLD  4324  noelOLD  4327  rabnc  4383  ralnralall  4514  imadif  6631  fiint  9342  kmlem16  10182  zorn2lem4  10516  nnunb  12492  indstr  12924  bwth  23307  lgsquadlem2  27307  frgrregord013  30198  difrab2  32289  ifeqeqx  32326  ballotlemodife  34107  sgn3da  34151  sbn1ALT  36325  poimirlem30  37112  clsk1indlem4  43446  atnaiana  46277  plcofph  46298