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  4055  dfnul4  4284  dfnul3  4286  rabnc  4344  ralnralall  4472  imadif  6621  fiint  9300  kmlem16  10172  zorn2lem4  10505  nnunb  12528  indstr  12969  sgn3da  15178  bwth  23641  lgsquadlem2  27625  frgrregord013  30883  difrab2  32981  ifeqeqx  33025  ballotlemodife  35017  sbn1ALT  37609  poimirlem30  38407  clsk1indlem4  44892  atnaiana  47819  plcofph  47840