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  1038  pssirrOLD  4060  dfnul4  4290  dfnul3  4292  rabnc  4348  ralnralall  4470  imadif  6609  fiint  9274  kmlem16  10137  zorn2lem4  10471  nnunb  12488  indstr  12928  sgn3da  15126  bwth  23524  lgsquadlem2  27499  frgrregord013  30651  difrab2  32750  ifeqeqx  32794  ballotlemodife  34800  sbn1ALT  37350  poimirlem30  38156  clsk1indlem4  44627  atnaiana  47516  plcofph  47537