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 233	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 210  df-an 400

This theorem is referenced by:  pm4.43  1020  pssirr  4028  indifdir  4210  dfnul2  4245  dfnul3  4246  noel  4247  rabnc  4295  ralnralall  4416  imadif  6408  fiint  8779  kmlem16  9576  zorn2lem4  9910  nnunb  11881  indstr  12304  bwth  22015  lgsquadlem2  25965  frgrregord013  28180  difrab2  30268  ifeqeqx  30309  ballotlemodife  31865  sgn3da  31909  poimirlem30  35087  clsk1indlem4  40747  atnaiana  43516  plcofph  43537