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  4056  dfnul4  4288  dfnul3  4290  rabnc  4344  ralnralall  4468  imadif  6570  fiint  9235  fiintOLD  9236  kmlem16  10079  zorn2lem4  10412  nnunb  12398  indstr  12835  bwth  23313  lgsquadlem2  27308  frgrregord013  30357  difrab2  32460  ifeqeqx  32504  sgn3da  32792  ballotlemodife  34465  sbn1ALT  36831  poimirlem30  37629  clsk1indlem4  44017  atnaiana  46908  plcofph  46929