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  4113  dfnul4  4341  dfnul3  4343  rabnc  4397  ralnralall  4521  imadif  6652  fiint  9364  fiintOLD  9365  kmlem16  10204  zorn2lem4  10537  nnunb  12520  indstr  12956  bwth  23434  lgsquadlem2  27440  frgrregord013  30424  difrab2  32526  ifeqeqx  32563  ballotlemodife  34479  sgn3da  34523  sbn1ALT  36841  poimirlem30  37637  clsk1indlem4  44034  atnaiana  46873  plcofph  46894