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 32745

Description: Virtual deduction proof of 3ornot23 32375. 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 32511	$/\$
4:1,?: e1a 32511	$/\$
5:3,4,?: e11 32572	$/\$ $\/$
6:2,?: e2 32515	$/\$ $\/$ $\/$ $\/$ $\/$
7:5,6,?: e12 32619	$/\$ $\/$ $\/$
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 32449	. . . . . 6 $/\$ $/\$
2		simpl 457	. . . . . 6 $/\$
3	1, 2	e1a 32511	. . . . 5 $/\$
4		simpr 461	. . . . . 6 $/\$
5	1, 4	e1a 32511	. . . . 5 $/\$
6		ioran 490	. . . . . 6 $\/$ $/\$
7	6	simplbi2 625	. . . . 5 $\/$
8	3, 5, 7	e11 32572	. . . 4 $/\$ $\/$
9		idn2 32497	. . . . 5 $/\$ $\/$ $\/$ $\/$ $\/$
10		3orass 976	. . . . . 6 $\/$ $\/$ $\/$ $\/$
11	10	biimpi 194	. . . . 5 $\/$ $\/$ $\/$ $\/$
12	9, 11	e2 32515	. . . 4 $/\$ $\/$ $\/$ $\/$ $\/$
13		orel2 383	. . . 4 $\/$ $\/$ $\/$
14	8, 12, 13	e12 32619	. . 3 $/\$ $\/$ $\/$
15	14	in2 32489	. 2 $/\$ $\/$ $\/$
16	15	in1 32446	1 $/\$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 972

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 185 df-or 370 df-an 371 df-3or 974 df-vd1 32445 df-vd2 32453

This theorem is referenced by: (None)

W3C validator