3ornot23VD - Mathbox for Alan Sare

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

Theorem 3ornot23VD 36882

Description: Virtual deduction proof of 3ornot23 36501. 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 36643	$/\$
4:1,?: e1a 36643	$/\$
5:3,4,?: e11 36704	$/\$ $\/$
6:2,?: e2 36647	$/\$ $\/$ $\/$ $\/$ $\/$
7:5,6,?: e12 36750	$/\$ $\/$ $\/$
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 36581	. . . . . 6 $/\$ $/\$
2		simpl 458	. . . . . 6 $/\$
3	1, 2	e1a 36643	. . . . 5 $/\$
4		simpr 462	. . . . . 6 $/\$
5	1, 4	e1a 36643	. . . . 5 $/\$
6		ioran 492	. . . . . 6 $\/$ $/\$
7	6	simplbi2 629	. . . . 5 $\/$
8	3, 5, 7	e11 36704	. . . 4 $/\$ $\/$
9		idn2 36629	. . . . 5 $/\$ $\/$ $\/$ $\/$ $\/$
10		3orass 985	. . . . . 6 $\/$ $\/$ $\/$ $\/$
11	10	biimpi 197	. . . . 5 $\/$ $\/$ $\/$ $\/$
12	9, 11	e2 36647	. . . 4 $/\$ $\/$ $\/$ $\/$ $\/$
13		orel2 384	. . . 4 $\/$ $\/$ $\/$
14	8, 12, 13	e12 36750	. . 3 $/\$ $\/$ $\/$
15	14	in2 36621	. 2 $/\$ $\/$ $\/$
16	15	in1 36578	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 369 $/\$ wa 370 $\/$ w3o 981

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 188 df-or 371 df-an 372 df-3or 983 df-vd1 36577 df-vd2 36585

This theorem is referenced by: (None)

W3C validator