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  1022  pssirr  3991  indifdirOLD  4176  dfnul4  4213  dfnul3  4215  dfnul2OLD  4216  dfnul3OLD  4217  noelOLD  4220  rabnc  4276  ralnralall  4405  imadif  6423  fiint  8869  kmlem16  9665  zorn2lem4  9999  nnunb  11972  indstr  12398  bwth  22161  lgsquadlem2  26117  frgrregord013  28332  difrab2  30419  ifeqeqx  30459  ballotlemodife  32034  sgn3da  32078  sbn1ALT  34673  poimirlem30  35430  clsk1indlem4  41200  atnaiana  43957  plcofph  43978