Type  Label  Description 
Statement 

Theorem  csbeq2gVD 27801 
Virtual deduction proof of csbeq2g 27451.
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. csbeq2g 27451
is csbeq2gVD 27801 without virtual deductions and was automatically derived
from csbeq2gVD 27801.
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 27802 
Virtual deduction proof of csbsng 3666.
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. csbsng 3666
is csbsngVD 27802 without virtual deductions and was automatically derived
from csbsngVD 27802.
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 27803 
Virtual deduction proof of csbxpg 4704.
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. csbxpg 4704
is csbxpgVD 27803 without virtual deductions and was automatically derived
from csbxpgVD 27803.
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 27804 
Virtual deduction proof of csbresg 4946.
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. csbresg 4946
is csbresgVD 27804 without virtual deductions and was automatically derived
from csbresgVD 27804.
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: 
 13:: 
 14:12,13: 
 qed:14: 

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



Theorem  csbrngVD 27805 
Virtual deduction proof of csbrng 4911.
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. csbrng 4911
is csbrngVD 27805 without virtual deductions and was automatically derived
from csbrngVD 27805.
1:: 
 2:1: 
 3:1: 
 4:3: 
 5:2,4: 
 6:5: 
 7:6: 
 8:1: 
 9:7,8: 
 10:9: 
 11:10: 
 12:1: 
 13:11,12: 
 14:: 
 15:14: 
 16:1,15: 
 17:13,16: 
 18:: 
 19:17,18: 
 qed:19: 

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



Theorem  csbima12gALTVD 27806 
Virtual deduction proof of csbima12gALT 5011.
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. csbima12gALT 5011
is csbima12gALTVD 27806 without virtual deductions and was automatically
derived
from csbima12gALTVD 27806.
1:: 
 2:1: 
 3:2: 
 4:1: 
 5:3,4: 
 6:: 
 7:6: 
 8:1,7: 
 9:5,8: 
 10:: 
 11:9,10: 
 qed:11: 

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



Theorem  csbunigVD 27807 
Virtual deduction proof of csbunig 3809.
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. csbunig 3809
is csbunigVD 27807 without virtual deductions and was automatically derived
from csbunigVD 27807.
1:: 
 2:1: 
 3:1: 
 4:2,3: 
 5:1: 
 6:4,5: 
 7:6: 
 8:7: 
 9:1: 
 10:8,9: 
 11:10: 
 12:11: 
 13:1: 
 14:12,13: 
 15:: 
 16:15: 
 17:1,16: 
 18:1,17: 
 19:14,18: 
 20:: 
 21:19,20: 
 qed:21: 

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



Theorem  csbfv12gALTVD 27808 
Virtual deduction proof of csbfv12gALT 5469.
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. csbfv12gALT 5469
is csbfv12gALTVD 27808 without virtual deductions and was automatically
derived
from csbfv12gALTVD 27808.
1:: 
 2:1: 
 3:1: 
 4:1: 
 5:4: 
 6:3,5: 
 7:1: 
 8:6,2: 
 9:7,8: 
 10:9: 
 11:10: 
 12:1: 
 13:11,12: 
 14:13: 
 15:1: 
 16:14,15: 
 17:: 
 18:17: 
 19:1,18: 
 20:16,19: 
 21:: 
 22:20,21: 
 qed:22: 

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



Theorem  con5VD 27809 
Virtual deduction proof of con5 27421.
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. con5 27421
is con5VD 27809 without virtual deductions and was automatically derived
from con5VD 27809.
1:: 
 2:1: 
 3:2: 
 4:: 
 5:3,4: 
 qed:5: 

(Contributed by Alan Sare, 21Apr2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  relopabVD 27810 
Virtual deduction proof of relopab 4800.
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. relopab 4800
is relopabVD 27810 without virtual deductions and was automatically derived
from relopabVD 27810.
1:: 
 2:1: 
 3:: 
 4:3: 
 5:2,4: 
 6:5: 
 7:6: 
 8:7: 
 9:8: 
 90:: 
 91:90: 
 92:: 
 10:91,92: 
 11:9,10: 
 12:11: 
 13:: 
 14:12,13: 
 15:14: 
 150:: 
 151:150: 
 152:: 
 16:151,152: 
 17:15,16: 
 18:17: 
 19:18: 
 20:: 
 21:19,20: 
 22:21: 
 23:: 
 24:22,23: 
 25:24: 
 26:: 
 27:: 
 28:26,27: 
 29:28: 
 30:29: 
 31:30: 
 32:31: 
 320:25,32: 
 33:: 
 34:: 
 35:33,34: 
 36:35: 
 37:36: 
 38:37: 
 39:38: 
 40:320,39: 
 41:: 
 42:: 
 43:40,41,42: 
 44:: 
 45:43,44: 
 46:28: 
 47:46: 
 48:45,47: 
 qed:48: 

(Contributed by Alan Sare, 9Jul2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  19.41rgVD 27811 
Virtual deduction proof of 19.41rg 27452.
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. 19.41rg 27452
is 19.41rgVD 27811 without virtual deductions and was automatically derived
from 19.41rgVD 27811. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:2: 
 4:3: 
 5:: 
 6:4,5: 
 7:: 
 8:6,7: 
 9:8: 
 10:9: 
 11:5: 
 12:10,11: 
 13:12: 
 14:13: 
 qed:14: 




Theorem  2pm13.193VD 27812 
Virtual deduction proof of 2pm13.193 27454.
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. 2pm13.193 27454
is 2pm13.193VD 27812 without virtual deductions and was automatically
derived from 2pm13.193VD 27812. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:2: 
 4:1: 
 5:3,4: 
 6:5: 
 7:6: 
 8:2: 
 9:7,8: 
 10:9: 
 11:10: 
 12:2,11: 
 13:12: 
 14:: 
 15:14: 
 16:15: 
 17:14: 
 18:16,17: 
 19:18: 
 20:15: 
 21:19: 
 22:20,21: 
 23:22: 
 24:23: 
 25:15,24: 
 26:25: 
 qed:13,26: 




Theorem  hbimpgVD 27813 
Virtual deduction proof of hbimpg 27456.
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. hbimpg 27456
is hbimpgVD 27813 without virtual deductions and was automatically derived
from hbimpgVD 27813. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:: 
 4:2: 
 5:4: 
 6:3,5: 
 7:: 
 8:7: 
 9:6,8: 
 10:9: 
 11:: 
 12:11: 
 13:1: 
 14:13: 
 15:14,12: 
 16:10,15: 
 17:: 
 18:16,17: 
 19:: 
 20:: 
 21:19,20: 
 22:21,18: 
 qed:22: 




Theorem  hbalgVD 27814 
Virtual deduction proof of hbalg 27457.
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. hbalg 27457
is hbalgVD 27814 without virtual deductions and was automatically derived
from hbalgVD 27814. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:: 
 4:2,3: 
 5:: 
 6:5,4: 
 qed:6: 




Theorem  hbexgVD 27815 
Virtual deduction proof of hbexg 27458.
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. hbexg 27458
is hbexgVD 27815 without virtual deductions and was automatically derived
from hbexgVD 27815. (Contributed by Alan Sare, 8Feb2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:2: 
 4:3: 
 5:: 
 6:: 
 7:5: 
 8:5,6,7: 
 9:8,4: 
 10:9: 
 11:10: 
 12:11: 
 13:12: 
 14:: 
 15:13,14: 
 16:15: 
 17:16: 
 18:: 
 19:17,18: 
 20:18: 
 21:19,20: 
 22:8,21: 
 23:14,22: 
 qed:23: 




Theorem  a9e2eqVD 27816* 
The following User's Proof is a Virtual Deduction proof (see: wvd1 27473)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. a9e2eq 27459 is a9e2eqVD 27816 without virtual
deductions and was automatically derived from a9e2eqVD 27816. (Contributed
by Alan Sare, 25Mar2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:: 
 3:1: 
 4:2,3: 
 5:2,4: 
 6:5: 
 7:6: 
 8:7: 
 9:: 
 10:8,9: 
 11:1,10: 
 12:11: 
 13:: 
 14:13,12: 
 140:14: 
 141:140: 
 15:1,141: 
 16:1,15: 
 17:16: 
 18:17: 
 19:: 
 20:: 
 21:20: 
 22:19,21: 
 23:20: 
 24:22,23: 
 25:24: 
 26:25: 
 27:26: 
 28:27: 
 29:28: 
 30:29: 
 31:18,30: 
 qed:31: 




Theorem  a9e2ndVD 27817* 
The following User's Proof is a Virtual Deduction proof (see: wvd1 27473)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. a9e2eq 27459 is a9e2ndVD 27817 without virtual
deductions and was automatically derived from a9e2ndVD 27817. (Contributed
by Alan Sare, 25Mar2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:: 
 3:1,2: 
 4:3: 
 5:: 
 6:5: 
 7:6: 
 8:4,7: 
 9:: 
 10:: 
 11:: 
 12:11: 
 120:11: 
 13:9,10,120: 
 14:: 
 15:14,13: 
 16:15: 
 17:16: 
 18:: 
 19:17,18: 
 20:14,19: 
 21:20: 
 22:21: 
 23:22: 
 24:: 
 25:23,24: 
 26:14,25: 
 27:26: 
 28:8,27: 
 29:28: 
 qed:29: 




Theorem  a9e2ndeqVD 27818* 
The following User's Proof is a Virtual Deduction proof (see: wvd1 27473)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. a9e2eq 27459 is a9e2ndeqVD 27818 without virtual
deductions and was automatically derived from a9e2ndeqVD 27818.
(Contributed by Alan Sare, 25Mar2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:: 
 3:2: 
 4:1,3: 
 5:2: 
 6:4,5: 
 7:: 
 8:7: 
 9:: 
 10:8,9: 
 11:6,10: 
 12:11: 
 13:12: 
 14:13: 
 15:: 
 19:15: 
 20:14,19: 
 21:20: 
 22:21: 
 23:: 
 24:22,23: 
 25:: 
 26:25: 
 260:: 
 27:260: 
 270:26,27: 
 28:: 
 29:270,28: 
 30:24,29: 
 31:30: 
 32:31: 
 33:: 
 34:33: 
 35:34: 
 36:35: 
 37:: 
 38:32,36,37: 
 39:: 
 40:: 
 41:40: 
 42:: 
 43:39,41,42: 
 44:40,43: 
 qed:38,44: 




Theorem  2sb5ndVD 27819* 
The following User's Proof is a Virtual Deduction proof (see: wvd1 27473)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. 2sb5nd 27462 is 2sb5ndVD 27819 without virtual
deductions and was automatically derived from 2sb5ndVD 27819. (Contributed
by Alan Sare, 30Apr2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
1:: 
 2:1: 
 3:: 
 4:3: 
 5:4: 
 6:: 
 7:: 
 8:7: 
 9:6,8: 
 10:9: 
 11:5,10: 
 12:11: 
 13:: 
 14:: 
 15:14: 
 16:13,15: 
 17:16: 
 19:12,17: 
 20:19: 
 21:2,20: 
 22:21: 
 23:13: 
 24:22,23: 
 240:24: 
 241:: 
 242:241,240: 
 243:: 
 25:242,243: 
 26:: 
 qed:25,26: 




Theorem  2uasbanhVD 27820* 
The following User's Proof is a Virtual Deduction proof (see: wvd1 27473)
completed automatically by a Metamath tools program invoking mmj2 and
the Metamath Proof Assistant. 2uasbanh 27463 is 2uasbanhVD 27820 without virtual
deductions and was automatically derived from 2uasbanhVD 27820.
(Contributed by Alan Sare, 31May2014.)
(Proof modification is discouraged.) (New usage is discouraged.)
h1:: 
 100:1: 
 2:100: 
 3:2: 
 4:3: 
 5:4: 
 6:5: 
 7:3,6: 
 8:2: 
 9:5: 
 10:8,9: 
 101:: 
 102:101: 
 103:: 
 104:102,103: 
 11:7,10,104: 
 110:5: 
 12:11,110: 
 120:12: 
 13:1,120: 
 14:: 
 15:14: 
 16:14: 
 17:16: 
 18:15,17: 
 19:18: 
 20:19: 
 21:20: 
 22:16: 
 23:15,22: 
 24:23: 
 25:24: 
 26:25: 
 27:21,26: 
 qed:13,27: 




Theorem  e2ebindVD 27821 
The following User's Proof is a Virtual Deduction proof (see:
wvd1 27473) completed automatically by a Metamath tools program invoking
mmj2 and the Metamath Proof Assistant. e2ebind 27465 is e2ebindVD 27821 without
virtual deductions and was automatically derived from e2ebindVD 27821
1:: 
 2:1: 
 3:2: 
 4:: 
 5:3,4: 
 6:: 
 7:5,6: 
 8:7: 
 9:: 
 10:8,9: 
 11:: 
 12:11: 
 13:10,12: 
 14:13: 
 15:: 
 qed:14,15: 

(Contributed by Alan Sare, 27Nov2014.) (Proof modification is
discouraged.) (New usage is discouraged.)



18.23.6 Virtual Deduction transcriptions of
textbook proofs


Theorem  sb5ALTVD 27822* 
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitchstyle Natural Deduction proof of Unit 20
Excercise 3.a., which is sb5 1994, found in the "Answers to Starred
Exercises" on page 457 of "Understanding Symbolic Logic", Fifth
Edition (2008), by Virginia Klenk. The same proof may also be
interpreted as a Virtual Deduction Hilbertstyle axiomatic proof. It
was completed automatically by the tools program completeusersproof.cmd,
which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof
Assistant. sb5ALT 27424 is sb5ALTVD 27822 without virtual deductions and
was automatically derived from sb5ALTVD 27822.
1:: 
 2:: 
 3:1,2: 
 4:3: 
 5:4: 
 6:: 
 7:: 
 8:7: 
 9:7: 
 10:8,9: 
 101:: 
 11:101,10: 
 12:5,11: 
 qed:12: 

(Contributed by Alan Sare, 21Apr2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  vk15.4jVD 27823 
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitchstyle Natural Deduction proof of Unit 15
Excercise 4.f. found in the "Answers to Starred Exercises" on page 442
of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia
Klenk. The same proof may also be interpreted to be a Virtual Deduction
Hilbertstyle axiomatic proof. It was completed automatically by the
tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and
Norm Megill's Metamath Proof Assistant. vk15.4j 27427 is vk15.4jVD 27823
without virtual deductions and was automatically derived
from vk15.4jVD 27823. Step numbers greater than 25 are additional steps
necessary for the sequent calculus proof not contained in the
Fitchstyle proof. Otherwise, step i of the User's Proof corresponds to
step i of the Fitchstyle proof.
h1:: 
 h2:: 
 h3:: 
 4:: 
 5:4: 
 6:3: 
 7:: 
 8:7: 
 9:7: 
 10:5: 
 11:10,8: 
 12:11: 
 13:12: 
 14:2,13: 
 140:: 
 141:140: 
 142:: 
 143:142: 
 144:6,14,141,143: 
 15:1: 
 16:9: 
 161:: 
 162:6,16,141,161: 
 17:162: 
 18:15,17: 
 19:18: 
 20:144: 
 21:: 
 22:19: 
 23:21,22: 
 24:23: 
 240:: 
 241:20,24,141,240: 
 25:241: 
 qed:25: 

(Contributed by Alan Sare, 21Apr2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  notnot2ALTVD 27824 
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitchstyle Natural Deduction proof of Theorem 5 of
Section 14 of [Margaris] p. 59 ( which is notnot2 106). The same proof
may also be interpreted as a Virtual Deduction Hilbertstyle
axiomatic proof. It was completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant. notnot2ALT 27428 is notnot2ALTVD 27824
without virtual deductions and was automatically derived
from notnot2ALTVD 27824. Step i of the User's Proof corresponds to
step i of the Fitchstyle proof.
1:: 
 2:: 
 3:1: 
 4:: 
 5:3: 
 6:5,1: 
 qed:6: 

(Contributed by Alan Sare, 21Apr2013.) (Proof modification is
discouraged.) (New usage is discouraged.)



Theorem  con3ALTVD 27825 
The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitchstyle Natural Deduction proof of Theorem 7 of
Section 14 of [Margaris] p. 60 ( which is con3 128). The same proof
may also be interpreted to be a Virtual Deduction Hilbertstyle
axiomatic proof. It was completed automatically by the tools program
completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's
Metamath Proof Assistant. con3ALT 27429 is con3ALTVD 27825
without virtual deductions and was automatically derived
from con3ALTVD 27825. Step i of the User's Proof corresponds to
step i of the Fitchstyle proof.
1:: 
 2:: 
 3:: 
 4:2: 
 5:1,4: 
 6:: 
 7:6,5: 
 8:7: 
 9:: 
 10:8:   