Type  Label  Description 
Statement 

Theorem  tratrbVD 36901* 
Virtual deduction proof of tratrb 36537. 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,?: e1a 36647 
 3:1,?: e1a 36647 
 4:1,?: e1a 36647 
 5:: 
 6:5,?: e2 36651 
 7:5,?: e2 36651 
 8:2,7,4,?: e121 36676 
 9:2,6,8,?: e122 36673 
 10:: 
 11:6,7,10,?: e223 36655 
 12:11: 
 13:: 
 14:12,13,?: e20 36757 
 15:: 
 16:7,15,?: e23 36785 
 17:6,16,?: e23 36785 
 18:17: 
 19:: 
 20:18,19,?: e20 36757 
 21:3,?: e1a 36647 
 22:21,9,4,?: e121 36676 
 23:22,?: e2 36651 
 24:4,23,?: e12 36754 
 25:14,20,24,?: e222 36656 
 26:25: 
 27:: 
 28:27,?: e0a 36802 
 29:28,26: 
 30:: 
 31:30,?: e0a 36802 
 32:31,29: 
 33:32,?: e1a 36647 
 qed:33: 

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



Theorem  al2imVD 36902 
Virtual deduction proof of al2im 1682. 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,?: e1a 36647 
 3:: 
 4:2,3,?: e10 36714 
 qed:4: 

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



Theorem  syl5impVD 36903 
Virtual deduction proof of syl5imp 36509. 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,?: e1a 36647 
 3:: 
 4:3,2,?: e21 36760 
 5:4,?: e2 36651 
 6:5: 
 qed:6: 

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



Theorem  idiVD 36904 
Virtual deduction proof of idiALT 36472. 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 36905 
Closed form of ancoms 454. 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 453 is derived automatically from it.
(Contributed by Alan Sare, 25Dec2011.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  ssralv2VD 36906* 
Quantification restricted to a subclass for two quantifiers. ssralv 3531
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 36528 is ssralv2VD 36906 without
virtual deductions and was automatically derived from ssralv2VD 36906.
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 36907 
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 8125. 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 36538 is ordelordALTVD 36907
without virtual deductions and was automatically derived from
ordelordALTVD 36907 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 36908 
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 3617 is equncomVD 36908 without
virtual deductions and was automatically derived from equncomVD 36908.
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 36909 
Inference form of equncom 3617. 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 3618 is equncomiVD 36909 without
virtual deductions and was automatically derived from equncomiVD 36909.
(Contributed by Alan Sare, 18Feb2012.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  sucidALTVD 36910 
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 36911 is sucidALTVD 36910
without virtual deductions and was automatically derived from
sucidALTVD 36910. 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 8125.
h1:: 
 2:1: 
 3:2: 
 4:: 
 qed:3,4: 

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



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



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

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



Theorem  imbi12VD 36913 
Implication form of imbi12i 327.
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 323 is imbi12VD 36913 without virtual deductions and was automatically
derived from imbi12VD 36913.
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 36914 
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 36517 is imbi13VD 36914 without virtual deductions and was automatically
derived from imbi13VD 36914.
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 36915 
Distribution of class substitution over a leftnested implication.
Similar to sbcimg 3347.
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 36539 is sbcim2gVD 36915 without virtual deductions and was automatically
derived from sbcim2gVD 36915.
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 36916 
Implication form of sbcbiiOLD 36532.
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 36540 is sbcbiVD 36916 without virtual deductions and was automatically
derived from sbcbiVD 36916.
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 36917* 
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 36541 is trsbcVD 36917 without virtual deductions and was automatically
derived from trsbcVD 36917.
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 36918* 
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 36542 is truniALTVD 36918 without virtual deductions and was
automatically derived from truniALTVD 36918.
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 36919 
Nonvirtual deduction form of e33 36764.
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 36518 is ee33VD 36919 without virtual deductions and was automatically
derived from ee33VD 36919.
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 36920* 
The intersection of a class of transitive sets is transitive. Virtual
deduction proof of trintALT 36921.
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 36921 is trintALTVD 36920 without virtual deductions and was
automatically derived from trintALTVD 36920.
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 36921* 
The intersection of a class of transitive sets is transitive. Exercise
5(b) of [Enderton] p. 73. trintALT 36921 is an alternate proof of trint 4535.
trintALT 36921 is trintALTVD 36920 without virtual deductions and was
automatically derived from trintALTVD 36920 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 36922 
The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual
deduction proof of undif3 3740.
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 3740 is undif3VD 36922 without virtual deductions and was automatically
derived from undif3VD 36922.
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 36923 
Virtual deduction proof of sbcssg 3914.
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 3914 is sbcssgVD 36923 without virtual deductions and was automatically
derived from sbcssgVD 36923.
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 36924 
Virtual deduction proof of csbingOLD 36858.
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 36858 is csbingVD 36924 without virtual deductions and was
automatically derived from csbingVD 36924.
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 36925* 
Virtual deduction proof of onfrALTlem5 36548.
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 36548 is onfrALTlem5VD 36925 without virtual deductions and was
automatically derived from onfrALTlem5VD 36925.
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 36926* 
Virtual deduction proof of onfrALTlem4 36549.
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 36549 is onfrALTlem4VD 36926 without virtual deductions and was
automatically derived from onfrALTlem4VD 36926.
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 36927* 
Virtual deduction proof of onfrALTlem3 36550.
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 36550 is onfrALTlem3VD 36927 without virtual deductions and was
automatically derived from onfrALTlem3VD 36927.
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 36928 
Virtual deduction proof of simplbi2comt 630.
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 630 is simplbi2comtVD 36928 without virtual deductions and was
automatically derived from simplbi2comtVD 36928.
1:: 
 2:1: 
 3:2: 
 4:3: 
 qed:4: 

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



Theorem  onfrALTlem2VD 36929* 
Virtual deduction proof of onfrALTlem2 36552.
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 36552 is onfrALTlem2VD 36929 without virtual deductions and was
automatically derived from onfrALTlem2VD 36929.
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 36930* 
Virtual deduction proof of onfrALTlem1 36554.
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 36554 is onfrALTlem1VD 36930 without virtual deductions and was
automatically derived from onfrALTlem1VD 36930.
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 36931 
Virtual deduction proof of onfrALT 36555.
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 36555 is onfrALTVD 36931 without virtual deductions and was
automatically derived from onfrALTVD 36931.
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 36932 
Virtual deduction proof of csbeq2gOLD 36556.
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 36556 is csbeq2gVD 36932 without virtual deductions and was
automatically derived from csbeq2gVD 36932.
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 36933 
Virtual deduction proof of csbsng 4061.
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 4061 is csbsngVD 36933 without virtual deductions and was automatically
derived from csbsngVD 36933.
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 36934 
Virtual deduction proof of csbxpgOLD 36857.
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 36857 is csbxpgVD 36934 without virtual deductions and was
automatically derived from csbxpgVD 36934.
1:: 
 2:1: 
 3:1: 
 4:3: 
 5:2,4: 
 6:1:   