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  9299  kmlem16  10171  zorn2lem4  10504  nnunb  12527  indstr  12968  sgn3da  15176  bwth  23639  lgsquadlem2  27618  frgrregord013  30876  difrab2  32974  ifeqeqx  33018  ballotlemodife  35011  sbn1ALT  37603  poimirlem30  38401  clsk1indlem4  44886  atnaiana  47813  plcofph  47834