Type  Label  Description 
Statement 

Theorem  3impexpVD 27901 
Virtual deduction proof of 3impexp 1358. 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,2,?: e10 27736 
 4:3,?: e1_ 27668 
 5:4,?: e1_ 27668 
 6:5: 
 7:: 
 8:7,?: e1_ 27668 
 9:8,?: e1_ 27668 
 10:2,9,?: e01 27732 
 11:10: 
 qed:6,11,?: e00 27812 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3impexpbicomVD 27902 
Virtual deduction proof of 3impexpbicom 1359. 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,2,?: e10 27736 
 4:3,?: e1_ 27668 
 5:4: 
 6:: 
 7:6,?: e1_ 27668 
 8:7,2,?: e10 27736 
 9:8: 
 qed:5,9,?: e00 27812 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3impexpbicomiVD 27903 
Virtual deduction proof of 3impexpbicomi 1360. 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.
(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcoreleleqVD 27904* 
Virtual deduction proof of sbcoreleleq 27570. 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:1,?: e1_ 27668 
 3:1,?: e1_ 27668 
 4:1,?: e1_ 27668 
 5:2,3,4,?: e111 27715 
 6:1,?: e1_ 27668 
 7:5,6: e11 27729 
 qed:7: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  hbra2VD 27905* 
Virtual deduction proof of nfra2 2599. 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,2,?: e00 27812 
 4:2: 
 5:4,?: e0_ 27816 
 qed:3,5,?: e00 27812 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  tratrbVD 27906* 
Virtual deduction proof of tratrb 27571. 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:1,?: e1_ 27668 
 3:1,?: e1_ 27668 
 4:1,?: e1_ 27668 
 5:: 
 6:5,?: e2 27672 
 7:5,?: e2 27672 
 8:2,7,4,?: e121 27697 
 9:2,6,8,?: e122 27694 
 10:: 
 11:6,7,10,?: e223 27676 
 12:11: 
 13:: 
 14:12,13,?: e20 27771 
 15:: 
 16:7,15,?: e23 27799 
 17:6,16,?: e23 27799 
 18:17: 
 19:: 
 20:18,19,?: e20 27771 
 21:3,?: e1_ 27668 
 22:21,9,4,?: e121 27697 
 23:22,?: e2 27672 
 24:4,23,?: e12 27768 
 25:14,20,24,?: e222 27677 
 26:25: 
 27:: 
 28:27,?: e0_ 27816 
 29:28,26: 
 30:: 
 31:30,?: e0_ 27816 
 32:31,29: 
 33:32,?: e1_ 27668 
 qed:33: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  3ax5VD 27907 
Virtual deduction proof of 3ax5 27572. 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:1,?: e1_ 27668 
 3:: 
 4:2,3,?: e10 27736 
 qed:4: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  syl5impVD 27908 
Virtual deduction proof of syl5imp 27546. 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:1,?: e1_ 27668 
 3:: 
 4:3,2,?: e21 27774 
 5:4,?: e2 27672 
 6:5: 
 qed:6: 

(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  idiVD 27909 
Virtual deduction proof of idi 2. 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.
(Contributed by Alan Sare, 31Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ancomsimpVD 27910 
Closed form of ancoms 441. 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.
(Contributed by Alan Sare, 25Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ssralv2VD 27911* 
Quantification restricted to a subclass for two quantifiers. ssralv 3239
for two quantifiers. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ssralv2 27566 is ssralv2VD 27911 without
virtual deductions and was automatically derived from ssralv2VD 27911.
1:: 
 2:: 
 3:1: 
 4:3,2: 
 5:4: 
 6:5: 
 7:: 
 8:7,6: 
 9:1: 
 10:9,8: 
 11:10: 
 12:: 
 13:: 
 14:12,13,11: 
 15:14: 
 16:15: 
 qed:16: 

(Contributed by Alan Sare, 10Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ordelordALTVD 27912 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4414 using
the Axiom of Regularity indirectly through dford2 7317. dford2 is a
weaker definition of ordinal number. Given the Axiom of Regularity, it
need not be assumed that because this is inferred by the
Axiom of Regularity. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ordelordALT 27573 is ordelordALTVD 27912
without virtual deductions and was automatically derived from
ordelordALTVD 27912 using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
1:: 
 2:1: 
 3:1: 
 4:2: 
 5:2: 
 6:4,3: 
 7:6,6,5: 
 8:: 
 9:8: 
 10:9: 
 11:10: 
 12:11: 
 13:12: 
 14:13: 
 15:14,5: 
 16:4,15,3: 
 17:16,7: 
 qed:17: 

(Contributed by Alan Sare, 12Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  equncomVD 27913 
If a class equals the union of two other classes, then it equals the
union of those two classes commuted. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncom 3322 is equncomVD 27913 without
virtual deductions and was automatically derived from equncomVD 27913.
1:: 
 2:: 
 3:1,2: 
 4:3: 
 5:: 
 6:5,2: 
 7:6: 
 8:4,7: 

(Contributed by Alan Sare, 17Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  equncomiVD 27914 
Inference form of equncom 3322. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncomi 3323 is equncomiVD 27914 without
virtual deductions and was automatically derived from equncomiVD 27914.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 27915 
A set belongs to its successor. Alternate proof of sucid 4471.
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT 27916 is sucidALTVD 27915
without virtual deductions and was automatically derived from
sucidALTVD 27915. This proof illustrates that
completeusersproof.cmd will generate a Metamath proof from any
User's Proof which is "conventional" in the sense that no step
is a virtual deduction, provided that all necessary unification
theorems and transformation deductions are in set.mm.
completeusersproof.cmd automatically converts such a
conventional proof into a Virtual Deduction proof for which each
step happens to be a 0virtual hypothesis virtual deduction.
The user does not need to search for reference theorem labels or
deduction labels nor does he(she) need to use theorems and
deductions which unify with reference theorems and deductions in
set.mm. All that is necessary is that each theorem or deduction
of the User's Proof unifies with some reference theorem or
deduction in set.mm or is a semantic variation of some theorem
or deduction which unifies with some reference theorem or
deduction in set.mm. The definition of "semantic variation" has
not been precisely defined. If it is obvious that a theorem or
deduction has the same meaning as another theorem or deduction,
then it is a semantic variation of the latter theorem or
deduction. For example, step 4 of the User's Proof is a
semantic variation of the definition (axiom)
, which unifies with dfsuc 4398, a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of a another
theorem or deduction if it is obvious upon cursory inspection
that it has the same meaning as a weaker form of the latter
theorem or deduction. For example, the deduction
infers is a
semantic variation of the theorem
, which unifies with
the set.mm reference definition (axiom) dford2 7317.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALT 27916 
A set belongs to its successor. This proof was automatically derived
from sucidALTVD 27915 using translate_{without}_overwriting.cmd and
minimizing. (Contributed by Alan Sare, 18Feb2012.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  sucidVD 27917 
A set belongs to its successor. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools
program completeusersproof.cmd, which invokes Mel O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant. sucid 4471 is
sucidVD 27917 without virtual deductions and was automatically
derived from sucidVD 27917.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  imbi12VD 27918 
Implication form of imbi12i 318. The following User's Proof is a Virtual
Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi12 27554
is imbi12VD 27918 without virtual deductions and was automatically derived
from imbi12VD 27918.
1:: 
 2:: 
 3:: 
 4:1,3: 
 5:2,4: 
 6:5: 
 7:: 
 8:1,7: 
 9:2,8: 
 10:9: 
 11:6,10: 
 12:11: 
 qed:12: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  imbi13VD 27919 
Join three logical equivalences to form equivalence of implications. The
following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. imbi13 27555
is imbi13VD 27919 without virtual deductions and was automatically derived
from imbi13VD 27919.
1:: 
 2:: 
 3:: 
 4:2,3: 
 5:1,4: 
 6:5: 
 7:6: 
 qed:7: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcim2gVD 27920 
Distribution of class substitution over a leftnested implication.
Similar
to sbcimg 3034. The following User's Proof is a Virtual Deduction proof
completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcim2g 27574
is sbcim2gVD 27920 without virtual deductions and was automatically derived
from sbcim2gVD 27920.
1:: 
 2:: 
 3:1,2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:: 
 8:4,7: 
 9:1: 
 10:8,9: 
 11:10: 
 12:6,11: 
 qed:12: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcbiVD 27921 
Implication form of sbcbiiOLD 3049. The following User's Proof is a
Virtual
Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcbi 27575
is sbcbiVD 27921 without virtual deductions and was automatically derived
from sbcbiVD 27921.
1:: 
 2:: 
 3:1,2: 
 4:1,3: 
 5:4: 
 qed:5: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  trsbcVD 27922* 
Formulabuilding inference rule for class substitution, substituting a
class
variable for the set variable of the transitivity predicate. The
following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trsbc 27576
is trsbcVD 27922 without virtual deductions and was automatically derived
from trsbcVD 27922.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:1,2,3,4: 
 6:1: 
 7:5,6: 
 8:: 
 9:7,8: 
 10:: 
 11:10: 
 12:1,11: 
 13:9,12: 
 14:13: 
 15:14: 
 16:1: 
 17:15,16: 
 18:17: 
 19:18: 
 20:1: 
 21:19,20: 
 22:: 
 23:21,22: 
 24:: 
 25:24: 
 26:1,25: 
 27:23,26: 
 qed:27: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  truniALTVD 27923* 
The union of a class of transitive sets is transitive. The following
User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 27577
is truniALTVD 27923 without virtual deductions and was automatically derived
from truniALTVD 27923.
1:: 
 2:: 
 3:2: 
 4:2: 
 5:4: 
 6:: 
 7:6: 
 8:6: 
 9:1,8: 
 10:8,9: 
 11:3,7,10: 
 12:11,8: 
 13:12: 
 14:13: 
 15:14: 
 16:5,15: 
 17:16: 
 18:17: 
 19:18: 
 qed:19: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ee33VD 27924 
Nonvirtual deduction form of e33 27778. The following User's Proof is a
Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ee33 27556
is ee33VD 27924 without virtual deductions and was automatically derived
from ee33VD 27924.
h1:: 
 h2:: 
 h3:: 
 4:1,3: 
 5:4: 
 6:2,5: 
 7:6: 
 8:7: 
 qed:8: 

(Contributed by Alan Sare, 18Mar2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  trintALTVD 27925* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 27926.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trintALT 27926
is trintALTVD 27925 without virtual deductions and was automatically derived
from trintALTVD 27925.
1:: 
 2:: 
 3:2: 
 4:2: 
 5:4: 
 6:5: 
 7:: 
 8:7,6: 
 9:7,1: 
 10:7,9: 
 11:10,3,8: 
 12:11: 
 13:12: 
 14:13: 
 15:3,14: 
 16:15: 
 17:16: 
 18:17: 
 qed:18: 

(Contributed by Alan Sare, 17Apr2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  trintALT 27926* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 27926 is an alternative proof of
trint 4130. trintALT 27926 is trintALTVD 27925 without virtual deductions and was
automatically derived from trintALTVD 27925 using the tools program
translate..without..overwriting.cmd and Metamath's minimize command.
(Contributed by Alan Sare, 17Apr2012.)
(Proof modification is discouraged.) (New usage is discouraged.)



Theorem  undif3VD 27927 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3431.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 3431
is undif3VD 27927 without virtual deductions and was automatically derived
from undif3VD 27927.
1:: 
 2:: 
 3:2: 
 4:1,3: 
 5:: 
 6:5: 
 7:5: 
 8:6,7: 
 9:8: 
 10:: 
 11:10: 
 12:10: 
 13:11: 
 14:12: 
 15:13,14: 
 16:15: 
 17:9,16: 
 18:: 
 19:18: 
 20:18: 
 21:18: 
 22:21: 
 23:: 
 24:23: 
 25:24: 
 26:25: 
 27:10: 
 28:27: 
 29:: 
 30:29: 
 31:30: 
 32:31: 
 33:22,26: 
 34:28,32: 
 35:33,34: 
 36:: 
 37:36,35: 
 38:17,37: 
 39:: 
 40:39: 
 41:: 
 42:40,41: 
 43:: 
 44:43,42: 
 45:: 
 46:45,44: 
 47:4,38: 
 48:46,47: 
 49:48: 
 qed:49: 

(Contributed by Alan Sare, 17Apr2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sbcssVD 27928 
Virtual deduction proof of sbcss 3566.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sbcss 3566
is sbcssVD 27928 without virtual deductions and was automatically derived
from sbcssVD 27928.
1:: 
 2:1: 
 3:1: 
 4:2,3: 
 5:1: 
 6:4,5: 
 7:6: 
 8:7: 
 9:1: 
 10:8,9: 
 11:: 
 110:11: 
 12:1,110: 
 13:10,12: 
 14:: 
 15:13,14: 
 qed:15: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  csbingVD 27929 
Virtual deduction proof of csbing 3378.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbing 3378
is csbingVD 27929 without virtual deductions and was automatically derived
from csbingVD 27929.
1:: 
 2:: 
 20:2: 
 30:1,20: 
 3:1,30: 
 4:1: 
 5:3,4: 
 6:1: 
 7:1: 
 8:6,7: 
 9:1: 
 10:9,8: 
 11:10: 
 12:11: 
 13:5,12: 
 14:: 
 15:13,14: 
 qed:15: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  onfrALTlem5VD 27930* 
Virtual deduction proof of onfrALTlem5 27579.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem5 27579 is onfrALTlem5VD 27930 without virtual deductions and was
automatically derived
from onfrALTlem5VD 27930.
1:: 
 2:1: 
 3:2: 
 4:3: 
 5:: 
 6:4,5: 
 7:2: 
 8:: 
 9:8: 
 10:2,9: 
 11:7,10: 
 12:6,11: 
 13:2: 
 14:12,13: 
 15:2: 
 16:15,14: 
 17:2: 
 18:2: 
 19:2: 
 20:18,19: 
 21:17,20: 
 22:2: 
 23:2: 
 24:21,23: 
 25:22,24: 
 26:2: 
 27:25,26: 
 28:2: 
 29:27,28: 
 30:29: 
 31:30: 
 32:: 
 33:31,32: 
 34:2: 
 35:33,34: 
 36:: 
 37:36: 
 38:2,37: 
 39:35,38: 
 40:16,39: 
 41:2: 
 qed:40,41: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  onfrALTlem4VD 27931* 
Virtual deduction proof of onfrALTlem4 27580.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem4 27580
is onfrALTlem4VD 27931 without virtual deductions and was automatically
derived
from onfrALTlem4VD 27931.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:1: 
 6:4,5: 
 7:3,6: 
 8:1: 
 9:7,8: 
 10:2,9: 
 11:1: 
 12:11,10: 
 13:1: 
 qed:13,12: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  onfrALTlem3VD 27932* 
Virtual deduction proof of onfrALTlem3 27581.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem3 27581
is onfrALTlem3VD 27932 without virtual deductions and was automatically
derived
from onfrALTlem3VD 27932.
1:: 
 2:: 
 3:2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:6: 
 8:: 
 9:7,8: 
 10:9: 
 11:10: 
 12:: 
 13:12,8: 
 14:13,11: 
 15:: 
 16:14,15: 
 17:: 
 18:2: 
 19:18: 
 20:17,19: 
 qed:16,20: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  simplbi2comgVD 27933 
Virtual deduction proof of simplbi2comg 1365.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. simplbi2comg 1365
is simplbi2comgVD 27933 without virtual deductions and was automatically
derived
from simplbi2comgVD 27933.
1:: 
 2:1: 
 3:2: 
 4:3: 
 qed:4: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  onfrALTlem2VD 27934* 
Virtual deduction proof of onfrALTlem2 27583.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem2 27583
is onfrALTlem2VD 27934 without virtual deductions and was automatically
derived
from onfrALTlem2VD 27934.
1:: 
 2:1: 
 3:2: 
 4:: 
 5:: 
 6:5: 
 7:4: 
 8:6,7: 
 9:8: 
 10:9: 
 11:1: 
 12:11: 
 13:2: 
 14:10,12,13: 
 15:3,14: 
 16:13,15: 
 17:16: 
 18:17: 
 19:18: 
 20:: 
 21:20: 
 22:19,21: 
 23:20: 
 24:23: 
 25:22,24: 
 26:25: 
 27:26: 
 28:27: 
 29:: 
 30:29: 
 31:28,30: 
 qed:31: 

(Contributed by Alan Sare, 22Jul2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  onfrALTlem1VD 27935* 
Virtual deduction proof of onfrALTlem1 27585.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem1 27585
is onfrALTlem1VD 27935 without virtual deductions and was automatically
derived
from onfrALTlem1VD 27935.
