Theorem pm3.24 407

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

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

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 401

This theorem is referenced by:  pm4.43  1040  pssirrOLD  4059  dfnul4  4289  dfnul3  4291  rabnc  4349  ralnralall  4475  imadif  6622  fiint  9287  kmlem16  10150  zorn2lem4  10484  nnunb  12501  indstr  12941  sgn3da  15140  bwth  23548  lgsquadlem2  27526  frgrregord013  30727  difrab2  32825  ifeqeqx  32869  ballotlemodife  34869  sbn1ALT  37474  poimirlem30  38282  clsk1indlem4  44753  atnaiana  47643  plcofph  47664