Theorem pm3.24 660

Description: Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction").

Assertion

Ref	Expression
pm3.24	⊢ ¬ (φ ⋀ ¬ φ)

Proof of Theorem pm3.24

Step	Hyp	Ref	Expression
1		exmid 657	. 2 ⊢ (¬ φ ⋁ ¬ ¬ φ)
2		ianor 305	. 2 ⊢ (¬ (φ ⋀ ¬ φ) ↔ (¬ φ ⋁ ¬ ¬ φ))
3	1, 2	mpbir 190	1 ⊢ ¬ (φ ⋀ ¬ φ)

Syntax hints:  ¬ wn 2   ⋁ wo 222   ⋀ wa 223

This theorem is referenced by:  exists2 1461  pssirr 2149  pssn2lp 2150  dfnul2 2285  dfnul3 2286  axnul 2714  imadif 3580  fiint 4572  fiintOLD 4573  kmlem16 4790  zorn2lem4 4801  nnunb 6072  indstr 6462

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain