Theorem pm3.24 406

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

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

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 209  df-an 400

This theorem is referenced by:  pm4.43  1035  pssirrOLD  4055  dfnul4  4285  dfnul3  4287  rabnc  4342  ralnralall  4464  imadif  6599  fiint  9264  kmlem16  10115  zorn2lem4  10449  nnunb  12470  indstr  12910  sgn3da  15104  bwth  23457  lgsquadlem2  27432  frgrregord013  30553  difrab2  32655  ifeqeqx  32700  ballotlemodife  34755  sbn1ALT  37303  poimirlem30  38109  clsk1indlem4  44580  atnaiana  47477  plcofph  47498