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  4052  dfnul4  4281  dfnul3  4283  rabnc  4341  ralnralall  4469  imadif  6616  fiint  9302  kmlem16  10225  zorn2lem4  10558  nnunb  12583  indstr  13024  sgn3da  15234  bwth  23708  lgsquadlem2  27690  frgrregord013  30978  difrab2  33076  ifeqeqx  33120  ballotlemodife  35113  sbn1ALT  37740  poimirlem30  38536  clsk1indlem4  45003  atnaiana  47937  plcofph  47958