3ornot23VD - Mathbox for Alan Sare

Mathbox for Alan Sare

< Previous Next >
Related theorems
Unicode version

Theorem 3ornot23VD 16671

Description: Virtual deduction proof of 3ornot23 1281. 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,?: e1_ 16518	. $/\$ ⊢ .
4:1,?: e1_ 16518	. $/\$ ⊢ .
5:3,4,?: e11 16578	. $/\$ ⊢ $\/$ .
6:2,?: e2 16521	. $/\$ $\/$ $\/$ ⊢ $\/$ $\/$ .
7:5,6,?: e12 16593	. $/\$ $\/$ $\/$ ⊢ .
8:7:	. $/\$ ⊢ $\/$ $\/$ .
qed:8:	$/\$ $\/$ $\/$

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

**Proof of Theorem 3ornot23VD**
Step	Hyp	Ref	Expression
1		idn1 16484	. . . . . 6 . $/\$ ⊢ $/\$ .
2		simpl 346	. . . . . 6 $/\$
3	1, 2	e1_ 16518	. . . . 5 . $/\$ ⊢ .
4		simpr 350	. . . . . 6 $/\$
5	1, 4	e1_ 16518	. . . . 5 . $/\$ ⊢ .
6		ioran 331	. . . . . 6 $\/$ $/\$
7	6	simplbi2 466	. . . . 5 $\/$
8	3, 5, 7	e11 16578	. . . 4 . $/\$ ⊢ $\/$ .
9		idn2 16509	. . . . 5 . $/\$ $\/$ $\/$ ⊢ $\/$ $\/$ .
10		3orass 861	. . . . . 6 $\/$ $\/$ $\/$ $\/$
11	10	biimpi 168	. . . . 5 $\/$ $\/$ $\/$ $\/$
12	9, 11	e2 16521	. . . 4 . $/\$ $\/$ $\/$ ⊢ $\/$ $\/$ .
13		orel2 272	. . . 4 $\/$ $\/$ $\/$
14	8, 12, 13	e12 16593	. . 3 . $/\$ $\/$ $\/$ ⊢ .
15	14	in2 16506	. 2 . $/\$ ⊢ $\/$ $\/$ .
16	15	in1 16481	1 $/\$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3 $\/$ wo 239 $/\$ wa 240 $\/$ w3o 857

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

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-vd1 16480 df-vd2 16489