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  4034  dfnul4  4283  dfnul3  4285  rabnc  4344  ralnralall  4472  imadif  6649  fiint  9349  kmlem16  10274  zorn2lem4  10607  nnunb  12632  indstr  13073  sgn3da  15286  bwth  23761  lgsquadlem2  27741  frgrregord013  31029  difrab2  33169  ifeqeqx  33213  ballotlemodife  35213  mirimanofffr  36642  sbn1ALT  37961  poimirlem30  38773  clsk1indlem4  45247  atnaiana  48208  plcofph  48229