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  1020  pssirr  4035  indifdirOLD  4219  dfnul4  4258  dfnul3  4260  dfnul2OLD  4261  dfnul3OLD  4262  noelOLD  4265  rabnc  4321  ralnralall  4449  imadif  6518  fiint  9091  kmlem16  9921  zorn2lem4  10255  nnunb  12229  indstr  12656  bwth  22561  lgsquadlem2  26529  frgrregord013  28759  difrab2  30845  ifeqeqx  30885  ballotlemodife  32464  sgn3da  32508  sbn1ALT  35042  poimirlem30  35807  clsk1indlem4  41654  atnaiana  44418  plcofph  44439