pm3.24 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pm3.24 657

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 654	. 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 1457 pssirr 2143 pssn2lp 2144 dfnul2 2279 dfnul3 2280 axnul 2705 imadif 3570 fiint 4543 kmlem16 4763 zorn2lem4 4774 nnunb 6027 indstr 6406

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