Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbxpgVD Structured version   Unicode version

Theorem csbxpgVD 28943
Description: Virtual deduction proof of csbxpg 4897. 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 4897 is csbxpgVD 28943 without virtual deductions and was automatically derived from csbxpgVD 28943.
 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, 10-Nov-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
csbxpgVD

Proof of Theorem csbxpgVD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 28602 . . . . . . . . . . . . . . . . . . 19
2 sbcel12g 3258 . . . . . . . . . . . . . . . . . . 19
31, 2e1_ 28665 . . . . . . . . . . . . . . . . . 18
4 csbconstg 3257 . . . . . . . . . . . . . . . . . . . 20
51, 4e1_ 28665 . . . . . . . . . . . . . . . . . . 19
6 eleq1 2495 . . . . . . . . . . . . . . . . . . 19
75, 6e1_ 28665 . . . . . . . . . . . . . . . . . 18
8 bibi1 318 . . . . . . . . . . . . . . . . . . 19
98biimprd 215 . . . . . . . . . . . . . . . . . 18
103, 7, 9e11 28726 . . . . . . . . . . . . . . . . 17
11 sbcel12g 3258 . . . . . . . . . . . . . . . . . . 19
121, 11e1_ 28665 . . . . . . . . . . . . . . . . . 18
13 csbconstg 3257 . . . . . . . . . . . . . . . . . . . 20
141, 13e1_ 28665 . . . . . . . . . . . . . . . . . . 19
15 eleq1 2495 . . . . . . . . . . . . . . . . . . 19
1614, 15e1_ 28665 . . . . . . . . . . . . . . . . . 18
17 bibi1 318 . . . . . . . . . . . . . . . . . . 19
1817biimprd 215 . . . . . . . . . . . . . . . . . 18
1912, 16, 18e11 28726 . . . . . . . . . . . . . . . . 17
20 pm4.38 843 . . . . . . . . . . . . . . . . . 18
2120ex 424 . . . . . . . . . . . . . . . . 17
2210, 19, 21e11 28726 . . . . . . . . . . . . . . . 16
23 sbcang 3196 . . . . . . . . . . . . . . . . 17
241, 23e1_ 28665 . . . . . . . . . . . . . . . 16
25 bibi1 318 . . . . . . . . . . . . . . . . 17
2625biimprcd 217 . . . . . . . . . . . . . . . 16
2722, 24, 26e11 28726 . . . . . . . . . . . . . . 15
28 sbcg 3218 . . . . . . . . . . . . . . . 16
291, 28e1_ 28665 . . . . . . . . . . . . . . 15
30 pm4.38 843 . . . . . . . . . . . . . . . 16
3130expcom 425 . . . . . . . . . . . . . . 15
3227, 29, 31e11 28726 . . . . . . . . . . . . . 14
33 sbcang 3196 . . . . . . . . . . . . . . 15
341, 33e1_ 28665 . . . . . . . . . . . . . 14
35 bibi1 318 . . . . . . . . . . . . . . 15
3635biimprcd 217 . . . . . . . . . . . . . 14
3732, 34, 36e11 28726 . . . . . . . . . . . . 13
3837gen11 28654 . . . . . . . . . . . 12
39 exbi 1591 . . . . . . . . . . . 12
4038, 39e1_ 28665 . . . . . . . . . . 11
41 sbcexg 3203 . . . . . . . . . . . 12
421, 41e1_ 28665 . . . . . . . . . . 11
43 bibi1 318 . . . . . . . . . . . 12
4443biimprcd 217 . . . . . . . . . . 11
4540, 42, 44e11 28726 . . . . . . . . . 10
4645gen11 28654 . . . . . . . . 9
47 exbi 1591 . . . . . . . . 9
4846, 47e1_ 28665 . . . . . . . 8
49 sbcexg 3203 . . . . . . . . 9
501, 49e1_ 28665 . . . . . . . 8
51 bibi1 318 . . . . . . . . 9
5251biimprcd 217 . . . . . . . 8
5348, 50, 52e11 28726 . . . . . . 7
5453gen11 28654 . . . . . 6
55 abbi 2545 . . . . . . 7
5655biimpi 187 . . . . . 6
5754, 56e1_ 28665 . . . . 5
58 csbabg 3302 . . . . . 6
591, 58e1_ 28665 . . . . 5
60 eqeq2 2444 . . . . . 6
6160biimpd 199 . . . . 5
6257, 59, 61e11 28726 . . . 4
63 df-xp 4876 . . . . . . 7
64 df-opab 4259 . . . . . . 7
6563, 64eqtri 2455 . . . . . 6
6665ax-gen 1555 . . . . 5
67 csbeq2g 28573 . . . . 5
681, 66, 67e10 28732 . . . 4
69 eqeq2 2444 . . . . 5
7069biimpd 199 . . . 4
7162, 68, 70e11 28726 . . 3
72 df-xp 4876 . . . 4
73 df-opab 4259 . . . 4
7472, 73eqtri 2455 . . 3
75 eqeq2 2444 . . . 4
7675biimprcd 217 . . 3
7771, 74, 76e10 28732 . 2
7877in1 28599 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wal 1549  wex 1550   wceq 1652   wcel 1725  cab 2421  wsbc 3153  csb 3243  cop 3809  copab 4257   cxp 4868 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sbc 3154  df-csb 3244  df-opab 4259  df-xp 4876  df-vd1 28598
 Copyright terms: Public domain W3C validator