Theorem pm3.24 408

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 23	. 2 ⊢ (𝜑 → 𝜑)
2		iman 407	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 233	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm4.43  1040  pssirrOLD  4061  dfnul4  4291  dfnul3  4293  rabnc  4351  ralnralall  4479  imadif  6627  fiint  9296  kmlem16  10168  zorn2lem4  10501  nnunb  12518  indstr  12958  sgn3da  15164  bwth  23604  lgsquadlem2  27582  frgrregord013  30783  difrab2  32881  ifeqeqx  32925  ballotlemodife  34920  sbn1ALT  37534  poimirlem30  38342  clsk1indlem4  44811  atnaiana  47701  plcofph  47722