Theorem pm3.24 922

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 439	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 219	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  pm4.43  964  pssirr  3669  indifdir  3842  dfnul2  3876  dfnul3  3877  rabnc  3916  imadif  5887  fiint  8122  kmlem16  8870  zorn2lem4  9204  nnunb  11165  indstr  11632  zeneo  14901  bwth  21023  lgsquadlem2  24906  frgrareg  26644  frgraregord013  26645  ifeqeqx  28745  ballotlemodife  29886  sgn3da  29930  poimirlem30  32609  clsk1indlem4  37362  atnaiana  39739  plcofph  39760  ralnralall  40307  av-frgraregord013  41549