Type  Label  Description 
Statement 

Theorem  orbi1rVD 28301 
Virtual deduction proof of orbi1r 27935. 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:2,?: e2 28073 
 4:1,3,?: e12 28177 
 5:4,?: e2 28073 
 6:5: 
 7:: 
 8:7,?: e2 28073 
 9:1,8,?: e12 28177 
 10:9,?: e2 28073 
 11:10: 
 12:6,11,?: e11 28130 
 qed:12: 

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



Theorem  bitr3VD 28302 
Virtual deduction proof of bitr3 27936. 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_ 28069 
 3:: 
 4:3,?: e2 28073 
 5:2,4,?: e12 28177 
 6:5: 
 qed:6: 

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



Theorem  3orbi123VD 28303 
Virtual deduction proof of 3orbi123 27937. 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_ 28069 
 3:1,?: e1_ 28069 
 4:1,?: e1_ 28069 
 5:2,3,?: e11 28130 
 6:5,4,?: e11 28130 
 7:?: 
 8:6,7,?: e10 28136 
 9:?: 
 10:8,9,?: e10 28136 
 qed:10: 

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



Theorem  sbc3orgVD 28304 
Virtual deduction proof of sbc3org 27959. 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_ 28069 
 3:: 
 32:3: 
 33:1,32,?: e10 28136 
 4:1,33,?: e11 28130 
 5:2,4,?: e11 28130 
 6:1,?: e1_ 28069 
 7:6,?: e1_ 28069 
 8:5,7,?: e11 28130 
 9:?: 
 10:8,9,?: e10 28136 
 qed:10: 

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



Theorem  19.21a3con13vVD 28305* 
Virtual deduction proof of alrim3con13v 27960. 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:2,?: e2 28073 
 4:2,?: e2 28073 
 5:2,?: e2 28073 
 6:1,4,?: e12 28177 
 7:3,?: e2 28073 
 8:5,?: e2 28073 
 9:7,6,8,?: e222 28078 
 10:9,?: e2 28073 
 11:10:in2 
 qed:11:in1 

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



Theorem  exbirVD 28306 
Virtual deduction proof of exbir 1371. 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:: 
 5:1,2,?: e12 28177 
 6:3,5,?: e32 28211 
 7:6: 
 8:7: 
 9:8,?: e1_ 28069 
 qed:9: 

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



Theorem  exbiriVD 28307 
Virtual deduction proof of exbiri 606. 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.
h1:: 
 2:: 
 3:: 
 4:: 
 5:2,1,?: e10 28136 
 6:3,5,?: e21 28183 
 7:4,6,?: e32 28211 
 8:7: 
 9:8: 
 qed:9: 

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



Theorem  rspsbc2VD 28308* 
Virtual deduction proof of rspsbc2 27961. 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:: 
 4:1,3,?: e13 28201 
 5:1,4,?: e13 28201 
 6:2,5,?: e23 28208 
 7:6: 
 8:7: 
 qed:8: 

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



Theorem  3impexpVD 28309 
Virtual deduction proof of 3impexp 1372. 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 28136 
 4:3,?: e1_ 28069 
 5:4,?: e1_ 28069 
 6:5: 
 7:: 
 8:7,?: e1_ 28069 
 9:8,?: e1_ 28069 
 10:2,9,?: e01 28133 
 11:10: 
 qed:6,11,?: e00 28221 

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



Theorem  3impexpbicomVD 28310 
Virtual deduction proof of 3impexpbicom 1373. 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 28136 
 4:3,?: e1_ 28069 
 5:4: 
 6:: 
 7:6,?: e1_ 28069 
 8:7,2,?: e10 28136 
 9:8: 
 qed:5,9,?: e00 28221 

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



Theorem  3impexpbicomiVD 28311 
Virtual deduction proof of 3impexpbicomi 1374. 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 28312* 
Virtual deduction proof of sbcoreleleq 27962. 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_ 28069 
 3:1,?: e1_ 28069 
 4:1,?: e1_ 28069 
 5:2,3,4,?: e111 28116 
 6:1,?: e1_ 28069 
 7:5,6: e11 28130 
 qed:7: 

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



Theorem  hbra2VD 28313* 
Virtual deduction proof of nfra2 2703. 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 28221 
 4:2: 
 5:4,?: e0_ 28225 
 qed:3,5,?: e00 28221 

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



Theorem  tratrbVD 28314* 
Virtual deduction proof of tratrb 27963. 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_ 28069 
 3:1,?: e1_ 28069 
 4:1,?: e1_ 28069 
 5:: 
 6:5,?: e2 28073 
 7:5,?: e2 28073 
 8:2,7,4,?: e121 28098 
 9:2,6,8,?: e122 28095 
 10:: 
 11:6,7,10,?: e223 28077 
 12:11: 
 13:: 
 14:12,13,?: e20 28180 
 15:: 
 16:7,15,?: e23 28208 
 17:6,16,?: e23 28208 
 18:17: 
 19:: 
 20:18,19,?: e20 28180 
 21:3,?: e1_ 28069 
 22:21,9,4,?: e121 28098 
 23:22,?: e2 28073 
 24:4,23,?: e12 28177 
 25:14,20,24,?: e222 28078 
 26:25: 
 27:: 
 28:27,?: e0_ 28225 
 29:28,26: 
 30:: 
 31:30,?: e0_ 28225 
 32:31,29: 
 33:32,?: e1_ 28069 
 qed:33: 

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



Theorem  3ax5VD 28315 
Virtual deduction proof of 3ax5 27964. 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_ 28069 
 3:: 
 4:2,3,?: e10 28136 
 qed:4: 

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



Theorem  syl5impVD 28316 
Virtual deduction proof of syl5imp 27938. 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_ 28069 
 3:: 
 4:3,2,?: e21 28183 
 5:4,?: e2 28073 
 6:5: 
 qed:6: 

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



Theorem  idiVD 28317 
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 28318 
Closed form of ancoms 440. 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 28319* 
Quantification restricted to a subclass for two quantifiers. ssralv 3350
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 27958 is ssralv2VD 28319 without
virtual deductions and was automatically derived from ssralv2VD 28319.
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 28320 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 4544 using
the Axiom of Regularity indirectly through dford2 7508. 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 27965 is ordelordALTVD 28320
without virtual deductions and was automatically derived from
ordelordALTVD 28320 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 28321 
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 3435 is equncomVD 28321 without
virtual deductions and was automatically derived from equncomVD 28321.
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 28322 
Inference form of equncom 3435. 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 3436 is equncomiVD 28322 without
virtual deductions and was automatically derived from equncomiVD 28322.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 28323 
A set belongs to its successor. Alternate proof of sucid 4601.
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 28324 is sucidALTVD 28323
without virtual deductions and was automatically derived from
sucidALTVD 28323. 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 4528, a
reference definition (axiom) in set.mm. Also, a theorem or
deduction is said to be a semantic variation of 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 7508.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



Theorem  sucidVD 28325 
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 4601 is
sucidVD 28325 without virtual deductions and was automatically
derived from sucidVD 28325.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



Theorem  imbi12VD 28326 
Implication form of imbi12i 317. 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 27946
is imbi12VD 28326 without virtual deductions and was automatically derived
from imbi12VD 28326.
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 28327 
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 27947
is imbi13VD 28327 without virtual deductions and was automatically derived
from imbi13VD 28327.
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 28328 
Distribution of class substitution over a leftnested implication.
Similar
to sbcimg 3145. 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 27966
is sbcim2gVD 28328 without virtual deductions and was automatically derived
from sbcim2gVD 28328.
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 28329 
Implication form of sbcbiiOLD 3160. 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 27967
is sbcbiVD 28329 without virtual deductions and was automatically derived
from sbcbiVD 28329.
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 28330* 
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 27968
is trsbcVD 28330 without virtual deductions and was automatically derived
from trsbcVD 28330.
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 28331* 
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 27969
is truniALTVD 28331 without virtual deductions and was automatically derived
from truniALTVD 28331.
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 28332 
Nonvirtual deduction form of e33 28187. 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 27948
is ee33VD 28332 without virtual deductions and was automatically derived
from ee33VD 28332.
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 28333* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 28334.
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 28334
is trintALTVD 28333 without virtual deductions and was automatically derived
from trintALTVD 28333.
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 28334* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 28334 is an alternative proof of
trint 4258. trintALT 28334 is trintALTVD 28333 without virtual deductions and was
automatically derived from trintALTVD 28333 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 28335 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3545.
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 3545
is undif3VD 28335 without virtual deductions and was automatically derived
from undif3VD 28335.
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 28336 
Virtual deduction proof of sbcss 3681.
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 3681
is sbcssVD 28336 without virtual deductions and was automatically derived
from sbcssVD 28336.
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 28337 
Virtual deduction proof of csbing 3491.
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 3491
is csbingVD 28337 without virtual deductions and was automatically derived
from csbingVD 28337.
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 28338* 
Virtual deduction proof of onfrALTlem5 27971.
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 27971 is onfrALTlem5VD 28338 without virtual deductions and was
automatically derived
from onfrALTlem5VD 28338.
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 28339* 
Virtual deduction proof of onfrALTlem4 27972.
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 27972
is onfrALTlem4VD 28339 without virtual deductions and was automatically
derived
from onfrALTlem4VD 28339.
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 28340* 
Virtual deduction proof of onfrALTlem3 27973.
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 27973
is onfrALTlem3VD 28340 without virtual deductions and was automatically
derived
from onfrALTlem3VD 28340.
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:   