pm2.13 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pm2.13 657

Description: Theorem *2.13 of [WhiteheadRussell] p. 101.

**Assertion**
Ref	Expression
pm2.13	$\/$

**Proof of Theorem pm2.13**
Step	Hyp	Ref	Expression
1		negb 86	. 2
2	1	orri 231	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 2 $\/$ wo 222

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