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  4055  dfnul4  4287  dfnul3  4289  rabnc  4343  ralnralall  4466  imadif  6576  fiint  9227  kmlem16  10076  zorn2lem4  10409  nnunb  12397  indstr  12829  bwth  23354  lgsquadlem2  27348  frgrregord013  30470  difrab2  32572  ifeqeqx  32617  sgn3da  32915  ballotlemodife  34655  sbn1ALT  37059  poimirlem30  37847  clsk1indlem4  44281  atnaiana  47165  plcofph  47186