Theorem pm3.24 405

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 22	. 2 ⊢ (𝜑 → 𝜑)
2		iman 404	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 232	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  pm4.43  1019  pssirr  4080  indifdir  4263  dfnul2  4296  dfnul2OLD  4297  dfnul3  4298  noel  4299  rabnc  4344  ralnralall  4461  imadif  6441  fiint  8798  kmlem16  9594  zorn2lem4  9924  nnunb  11896  indstr  12319  bwth  22021  lgsquadlem2  25960  frgrregord013  28177  difrab2  30264  ifeqeqx  30300  ballotlemodife  31759  sgn3da  31803  poimirlem30  34926  clsk1indlem4  40400  atnaiana  43166  plcofph  43187