Theorem pm3.24 403

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

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

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 208  df-an 397

This theorem is referenced by:  pm4.43  1030  pssirr  4041  dfnul4  4270  dfnul3  4272  rabnc  4326  ralnralall  4448  imadif  6576  fiint  9234  kmlem16  10086  zorn2lem4  10419  nnunb  12431  indstr  12864  bwth  23400  lgsquadlem2  27369  frgrregord013  30490  difrab2  32592  ifeqeqx  32637  sgn3da  32933  ballotlemodife  34689  sbn1ALT  37218  poimirlem30  38024  clsk1indlem4  44495  atnaiana  47393  plcofph  47414