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

Theorem csbxpgVD 37291
Description: Virtual deduction proof of csbxpgOLD 37214. 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 37214 is csbxpgVD 37291 without virtual deductions and was automatically derived from csbxpgVD 37291.
 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 36944 . . . . . . . . . . . . . . . . . . 19
2 sbcel12gOLD 36905 . . . . . . . . . . . . . . . . . . 19
31, 2e1a 37006 . . . . . . . . . . . . . . . . . 18
4 csbconstg 3376 . . . . . . . . . . . . . . . . . . . 20
51, 4e1a 37006 . . . . . . . . . . . . . . . . . . 19
6 eleq1 2517 . . . . . . . . . . . . . . . . . . 19
75, 6e1a 37006 . . . . . . . . . . . . . . . . . 18
8 bibi1 329 . . . . . . . . . . . . . . . . . . 19
98biimprd 227 . . . . . . . . . . . . . . . . . 18
103, 7, 9e11 37067 . . . . . . . . . . . . . . . . 17
11 sbcel12gOLD 36905 . . . . . . . . . . . . . . . . . . 19
121, 11e1a 37006 . . . . . . . . . . . . . . . . . 18
13 csbconstg 3376 . . . . . . . . . . . . . . . . . . . 20
141, 13e1a 37006 . . . . . . . . . . . . . . . . . . 19
15 eleq1 2517 . . . . . . . . . . . . . . . . . . 19
1614, 15e1a 37006 . . . . . . . . . . . . . . . . . 18
17 bibi1 329 . . . . . . . . . . . . . . . . . . 19
1817biimprd 227 . . . . . . . . . . . . . . . . . 18
1912, 16, 18e11 37067 . . . . . . . . . . . . . . . . 17
20 pm4.38 883 . . . . . . . . . . . . . . . . . 18
2120ex 436 . . . . . . . . . . . . . . . . 17
2210, 19, 21e11 37067 . . . . . . . . . . . . . . . 16
23 sbcangOLD 36890 . . . . . . . . . . . . . . . . 17
241, 23e1a 37006 . . . . . . . . . . . . . . . 16
25 bibi1 329 . . . . . . . . . . . . . . . . 17
2625biimprcd 229 . . . . . . . . . . . . . . . 16
2722, 24, 26e11 37067 . . . . . . . . . . . . . . 15
28 sbcg 3333 . . . . . . . . . . . . . . . 16
291, 28e1a 37006 . . . . . . . . . . . . . . 15
30 pm4.38 883 . . . . . . . . . . . . . . . 16
3130expcom 437 . . . . . . . . . . . . . . 15
3227, 29, 31e11 37067 . . . . . . . . . . . . . 14
33 sbcangOLD 36890 . . . . . . . . . . . . . . 15
341, 33e1a 37006 . . . . . . . . . . . . . 14
35 bibi1 329 . . . . . . . . . . . . . . 15
3635biimprcd 229 . . . . . . . . . . . . . 14
3732, 34, 36e11 37067 . . . . . . . . . . . . 13
3837gen11 36995 . . . . . . . . . . . 12
39 exbi 1716 . . . . . . . . . . . 12
4038, 39e1a 37006 . . . . . . . . . . 11
41 sbcexgOLD 36904 . . . . . . . . . . . 12
421, 41e1a 37006 . . . . . . . . . . 11
43 bibi1 329 . . . . . . . . . . . 12
4443biimprcd 229 . . . . . . . . . . 11
4540, 42, 44e11 37067 . . . . . . . . . 10
4645gen11 36995 . . . . . . . . 9
47 exbi 1716 . . . . . . . . 9
4846, 47e1a 37006 . . . . . . . 8
49 sbcexgOLD 36904 . . . . . . . . 9
501, 49e1a 37006 . . . . . . . 8
51 bibi1 329 . . . . . . . . 9
5251biimprcd 229 . . . . . . . 8
5348, 50, 52e11 37067 . . . . . . 7
5453gen11 36995 . . . . . 6
55 abbi 2565 . . . . . . 7
5655biimpi 198 . . . . . 6
5754, 56e1a 37006 . . . . 5
58 csbabgOLD 37211 . . . . . 6
591, 58e1a 37006 . . . . 5
60 eqeq2 2462 . . . . . 6
6160biimpd 211 . . . . 5
6257, 59, 61e11 37067 . . . 4
63 df-xp 4840 . . . . . . 7
64 df-opab 4462 . . . . . . 7
6563, 64eqtri 2473 . . . . . 6
6665ax-gen 1669 . . . . 5
67 csbeq2gOLD 36916 . . . . 5
681, 66, 67e10 37073 . . . 4
69 eqeq2 2462 . . . . 5
7069biimpd 211 . . . 4
7162, 68, 70e11 37067 . . 3
72 df-xp 4840 . . . 4
73 df-opab 4462 . . . 4
7472, 73eqtri 2473 . . 3
75 eqeq2 2462 . . . 4
7675biimprcd 229 . . 3
7771, 74, 76e10 37073 . 2
7877in1 36941 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371  wal 1442   wceq 1444  wex 1663   wcel 1887  cab 2437  wsbc 3267  csb 3363  cop 3974  copab 4460   cxp 4832 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-sbc 3268  df-csb 3364  df-opab 4462  df-xp 4840  df-vd1 36940 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator