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 39082

Description: Virtual deduction proof of 3ornot23 38715. 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 38852	$/\$
4:1,?: e1a 38852	$/\$
5:3,4,?: e11 38913	$/\$ $\/$
6:2,?: e2 38856	$/\$ $\/$ $\/$ $\/$ $\/$
7:5,6,?: e12 38951	$/\$ $\/$ $\/$
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 38790	. . . . . 6 $/\$ $/\$
2		simpl 473	. . . . . 6 $/\$
3	1, 2	e1a 38852	. . . . 5 $/\$
4		simpr 477	. . . . . 6 $/\$
5	1, 4	e1a 38852	. . . . 5 $/\$
6		ioran 511	. . . . . 6 $\/$ $/\$
7	6	simplbi2 655	. . . . 5 $\/$
8	3, 5, 7	e11 38913	. . . 4 $/\$ $\/$
9		idn2 38838	. . . . 5 $/\$ $\/$ $\/$ $\/$ $\/$
10		3orass 1040	. . . . . 6 $\/$ $\/$ $\/$ $\/$
11	10	biimpi 206	. . . . 5 $\/$ $\/$ $\/$ $\/$
12	9, 11	e2 38856	. . . 4 $/\$ $\/$ $\/$ $\/$ $\/$
13		orel2 398	. . . 4 $\/$ $\/$ $\/$
14	8, 12, 13	e12 38951	. . 3 $/\$ $\/$ $\/$
15	14	in2 38830	. 2 $/\$ $\/$ $\/$
16	15	in1 38787	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036

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 197 df-or 385 df-an 386 df-3or 1038 df-vd1 38786 df-vd2 38794

This theorem is referenced by: (None)

W3C validator