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 229	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 206  df-an 397

This theorem is referenced by:  pm4.43  1021  pssirr  4065  indifdirOLD  4250  dfnul4  4289  dfnul3  4291  dfnul2OLD  4292  dfnul3OLD  4293  noelOLD  4296  rabnc  4352  ralnralall  4481  imadif  6590  fiint  9275  kmlem16  10110  zorn2lem4  10444  nnunb  12418  indstr  12850  bwth  22798  lgsquadlem2  26766  frgrregord013  29402  difrab2  31490  ifeqeqx  31528  ballotlemodife  33186  sgn3da  33230  sbn1ALT  35400  poimirlem30  36181  clsk1indlem4  42438  atnaiana  45278  plcofph  45299