3ornot23VD - Mathbox for Alan Sare

	Mathbox for Alan Sare		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > 3ornot23VD		Structured version Visualization version Unicode version

Theorem 3ornot23VD 37243

Description: Virtual deduction proof of 3ornot23 36865. The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1::

$/\$ $/\$
2::	$/\$ $\/$ $\/$ $\/$ $\/$
3:1,?: e1a 37006	$/\$
4:1,?: e1a 37006	$/\$
5:3,4,?: e11 37067	$/\$ $\/$
6:2,?: e2 37010	$/\$ $\/$ $\/$ $\/$ $\/$
7:5,6,?: e12 37111	$/\$ $\/$ $\/$
8:7:	$/\$ $\/$ $\/$
qed:8:	$/\$ $\/$ $\/$

(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
3ornot23VD	$/\$ $\/$ $\/$

**Proof of Theorem 3ornot23VD**
Step	Hyp	Ref	Expression
1		idn1 36944	. . . . . 6 $/\$ $/\$
2		simpl 459	. . . . . 6 $/\$
3	1, 2	e1a 37006	. . . . 5 $/\$
4		simpr 463	. . . . . 6 $/\$
5	1, 4	e1a 37006	. . . . 5 $/\$
6		ioran 493	. . . . . 6 $\/$ $/\$
7	6	simplbi2 631	. . . . 5 $\/$
8	3, 5, 7	e11 37067	. . . 4 $/\$ $\/$
9		idn2 36992	. . . . 5 $/\$ $\/$ $\/$ $\/$ $\/$
10		3orass 988	. . . . . 6 $\/$ $\/$ $\/$ $\/$
11	10	biimpi 198	. . . . 5 $\/$ $\/$ $\/$ $\/$
12	9, 11	e2 37010	. . . 4 $/\$ $\/$ $\/$ $\/$ $\/$
13		orel2 385	. . . 4 $\/$ $\/$ $\/$
14	8, 12, 13	e12 37111	. . 3 $/\$ $\/$ $\/$
15	14	in2 36984	. 2 $/\$ $\/$ $\/$
16	15	in1 36941	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 370 $/\$ wa 371 $\/$ w3o 984

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

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-vd1 36940 df-vd2 36948

This theorem is referenced by: (None)

W3C validator