pm10.253 - Mathbox for Andrew Salmon

	Mathbox for Andrew Salmon		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > pm10.253		Structured version Visualization version Unicode version

Theorem pm10.253 38561

Description: Theorem *10.253 in [WhiteheadRussell] p. 149. (Contributed by Andrew Salmon, 17-Jun-2011.)

**Assertion**
Ref	Expression
pm10.253

**Proof of Theorem pm10.253**
Step	Hyp	Ref	Expression
1		alex 1753	. . 3
2	1	bicomi 214	. 2
3	2	con1bii 346	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196

wal 1481

wex 1704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737

This theorem depends on definitions: df-bi 197 df-ex 1705

This theorem is referenced by: (None)