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  4031  dfnul4  4280  dfnul3  4282  rabnc  4340  ralnralall  4468  imadif  6625  fiint  9322  kmlem16  10248  zorn2lem4  10581  nnunb  12606  indstr  13047  sgn3da  15260  bwth  23734  lgsquadlem2  27714  frgrregord013  31002  difrab2  33142  ifeqeqx  33186  ballotlemodife  35177  sbn1ALT  37863  poimirlem30  38662  clsk1indlem4  45138  atnaiana  48087  plcofph  48108