pm3.24 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pm3.24 661

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 658	. 2 $\/$
2		ianor 303	. 2 $/\$ $\/$
3	1, 2	mpbir 188	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 2 $\/$ wo 220 $/\$ wa 221

This theorem is referenced by: exists2 1499 pssirr 2198 pssn2lp 2199 dfnul2 2334 dfnul3 2335 axnul 2783 imadif 3679 fiint 4703 kmlem16 4926 zorn2lem4 4937 nnunb 6238 indstr 6588 ordtypelem4 11430

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 145 df-or 222 df-an 223