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  4052  dfnul4  4284  dfnul3  4286  rabnc  4340  ralnralall  4464  imadif  6570  fiint  9218  kmlem16  10064  zorn2lem4  10397  nnunb  12384  indstr  12816  bwth  23326  lgsquadlem2  27320  frgrregord013  30377  difrab2  32479  ifeqeqx  32524  sgn3da  32822  ballotlemodife  34532  sbn1ALT  36923  poimirlem30  37710  clsk1indlem4  44161  atnaiana  47047  plcofph  47068