Theorem pm3.24 402

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 401	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 230	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

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

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 207  df-an 396

This theorem is referenced by:  pm4.43  1024  pssirr  4102  dfnul4  4334  dfnul3  4336  rabnc  4390  ralnralall  4514  imadif  6649  fiint  9367  fiintOLD  9368  kmlem16  10207  zorn2lem4  10540  nnunb  12524  indstr  12959  bwth  23419  lgsquadlem2  27426  frgrregord013  30415  difrab2  32518  ifeqeqx  32556  ballotlemodife  34501  sgn3da  34545  sbn1ALT  36860  poimirlem30  37658  clsk1indlem4  44062  atnaiana  46940  plcofph  46961