Type  Label  Description 
Statement 

Theorem  idiVD 37301 
Virtual deduction proof of idiALT 36876. 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  ancomstVD 37302 
Closed form of ancoms 459. 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.
The proof of ancomst 458 is derived automatically from it.
(Contributed by Alan Sare, 25Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ssralv2VD 37303* 
Quantification restricted to a subclass for two quantifiers. ssralv 3505
for two quantifiers. The following User's Proof is a Virtual Deduction
proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ssralv2 36932 is ssralv2VD 37303 without
virtual deductions and was automatically derived from ssralv2VD 37303.
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 37304 
An element of an ordinal class is ordinal. Proposition 7.6 of
[TakeutiZaring] p. 36. This is an alternate proof of ordelord 5464 using
the Axiom of Regularity indirectly through dford2 8151. 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 L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. ordelordALT 36942 is ordelordALTVD 37304
without virtual deductions and was automatically derived from
ordelordALTVD 37304 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 37305 
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 L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncom 3591 is equncomVD 37305 without
virtual deductions and was automatically derived from equncomVD 37305.
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 37306 
Inference form of equncom 3591. The following User's Proof is a
Virtual Deduction proof completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. equncomi 3592 is equncomiVD 37306 without
virtual deductions and was automatically derived from equncomiVD 37306.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 37307 
A set belongs to its successor. Alternate proof of sucid 5521.
The following User's Proof is a Virtual Deduction proof
completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. sucidALT 37308 is sucidALTVD 37307
without virtual deductions and was automatically derived from
sucidALTVD 37307. 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 5448, 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 8151.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



Theorem  sucidVD 37309 
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 L. O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant.
sucid 5521 is sucidVD 37309 without virtual deductions and was automatically
derived from sucidVD 37309.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



Theorem  imbi12VD 37310 
Implication form of imbi12i 332.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
imbi12 328 is imbi12VD 37310 without virtual deductions and was automatically
derived from imbi12VD 37310.
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 37311 
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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
imbi13 36921 is imbi13VD 37311 without virtual deductions and was automatically
derived from imbi13VD 37311.
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 37312 
Distribution of class substitution over a leftnested implication.
Similar to sbcimg 3321.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
sbcim2g 36943 is sbcim2gVD 37312 without virtual deductions and was automatically
derived from sbcim2gVD 37312.
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 37313 
Implication form of sbcbiiOLD 36936.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
sbcbi 36944 is sbcbiVD 37313 without virtual deductions and was automatically
derived from sbcbiVD 37313.
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 37314* 
Formulabuilding inference rule for class substitution, substituting a
class variable for the setvar 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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
trsbc 36945 is trsbcVD 37314 without virtual deductions and was automatically
derived from trsbcVD 37314.
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 37315* 
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 L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
truniALT 36946 is truniALTVD 37315 without virtual deductions and was
automatically derived from truniALTVD 37315.
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 37316 
Nonvirtual deduction form of e33 37161.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
ee33 36922 is ee33VD 37316 without virtual deductions and was automatically
derived from ee33VD 37316.
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 37317* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 37318.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
trintALT 37318 is trintALTVD 37317 without virtual deductions and was
automatically derived from trintALTVD 37317.
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 37318* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 37318 is an alternate proof of trint 4526.
trintALT 37318 is trintALTVD 37317 without virtual deductions and was
automatically derived from trintALTVD 37317 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 37319 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3716.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
undif3 3716 is undif3VD 37319 without virtual deductions and was automatically
derived from undif3VD 37319.
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  sbcssgVD 37320 
Virtual deduction proof of sbcssg 3892.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
sbcssg 3892 is sbcssgVD 37320 without virtual deductions and was automatically
derived from sbcssgVD 37320.
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 37321 
Virtual deduction proof of csbingOLD 37255.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
csbingOLD 37255 is csbingVD 37321 without virtual deductions and was
automatically derived from csbingVD 37321.
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 37322* 
Virtual deduction proof of onfrALTlem5 36952.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem5 36952 is onfrALTlem5VD 37322 without virtual deductions and was
automatically derived from onfrALTlem5VD 37322.
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 37323* 
Virtual deduction proof of onfrALTlem4 36953.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem4 36953 is onfrALTlem4VD 37323 without virtual deductions and was
automatically derived from onfrALTlem4VD 37323.
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 37324* 
Virtual deduction proof of onfrALTlem3 36954.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem3 36954 is onfrALTlem3VD 37324 without virtual deductions and was
automatically derived from onfrALTlem3VD 37324.
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  simplbi2comtVD 37325 
Virtual deduction proof of simplbi2comt 636.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
simplbi2comt 636 is simplbi2comtVD 37325 without virtual deductions and was
automatically derived from simplbi2comtVD 37325.
1:: 
 2:1: 
 3:2: 
 4:3: 
 qed:4: 

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



Theorem  onfrALTlem2VD 37326* 
Virtual deduction proof of onfrALTlem2 36956.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem2 36956 is onfrALTlem2VD 37326 without virtual deductions and was
automatically derived from onfrALTlem2VD 37326.
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 37327* 
Virtual deduction proof of onfrALTlem1 36958.
The following User's Proof is a Virtual Deduction proof completed
automatically by the tools program completeusersproof.cmd, which invokes
Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
onfrALTlem1 36958 is onfrALTlem1VD 37327 without virtual deductions and was
automatically derived from onfrALTlem1VD 37327.
1:: 
 2:1: 
 3:2: 
 4:: 
 5:4: 
 6:5: 
 7:3,6: 
 8:: 
 qed:7,8: 

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



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

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



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

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



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

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



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

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



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