pm3.24 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

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 $/\$

Colors of variables: wff set class

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