Theorem pm3.24 401

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 400	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 229	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  pm4.43  1019  pssirr  4099  indifdirOLD  4284  dfnul4  4323  dfnul3  4325  dfnul2OLD  4326  dfnul3OLD  4327  noelOLD  4330  rabnc  4386  ralnralall  4517  imadif  6631  fiint  9326  kmlem16  10162  zorn2lem4  10496  nnunb  12472  indstr  12904  bwth  23134  lgsquadlem2  27120  frgrregord013  29915  difrab2  32005  ifeqeqx  32041  ballotlemodife  33794  sgn3da  33838  sbn1ALT  36040  poimirlem30  36821  clsk1indlem4  43097  atnaiana  45931  plcofph  45952