pm3.24 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pm3.24 656

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 653	. 2 $\/$
2		ianor 305	. 2 $/\$ $\/$
3	1, 2	mpbir 190	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 2 $\/$ wo 222 $/\$ wa 223

This theorem is referenced by: exists2 1451 pssirr 2136 pssn2lp 2137 dfnul2 2272 dfnul3 2273 axnul 2699 imadif 3560 fiint 4534 kmlem16 4752 zorn2lem4 4763 nnunb 6017 indstr 6393

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