Theorem pm3.24 404

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

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

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 206  df-an 398

This theorem is referenced by:  pm4.43  1022  pssirr  4101  indifdirOLD  4286  dfnul4  4325  dfnul3  4327  dfnul2OLD  4328  dfnul3OLD  4329  noelOLD  4332  rabnc  4388  ralnralall  4519  imadif  6633  fiint  9324  kmlem16  10160  zorn2lem4  10494  nnunb  12468  indstr  12900  bwth  22914  lgsquadlem2  26884  frgrregord013  29648  difrab2  31738  ifeqeqx  31774  ballotlemodife  33496  sgn3da  33540  sbn1ALT  35737  poimirlem30  36518  clsk1indlem4  42795  atnaiana  45633  plcofph  45654