Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cgsex4g Structured version   Unicode version

Theorem cgsex4g 2981
 Description: An implicit substitution inference for 4 general classes. (Contributed by NM, 5-Aug-1995.)
Hypotheses
Ref Expression
cgsex4g.1
cgsex4g.2
Assertion
Ref Expression
cgsex4g
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,
Allowed substitution hints:   (,,,)   (,,,)   (,,,)   (,,,)

Proof of Theorem cgsex4g
StepHypRef Expression
1 cgsex4g.2 . . . . 5
21biimpa 471 . . . 4
32exlimivv 1645 . . 3
43exlimivv 1645 . 2
5 elisset 2958 . . . . . . . 8
6 elisset 2958 . . . . . . . 8
75, 6anim12i 550 . . . . . . 7
8 eeanv 1937 . . . . . . 7
97, 8sylibr 204 . . . . . 6
10 elisset 2958 . . . . . . . 8
11 elisset 2958 . . . . . . . 8
1210, 11anim12i 550 . . . . . . 7
13 eeanv 1937 . . . . . . 7
1412, 13sylibr 204 . . . . . 6
159, 14anim12i 550 . . . . 5
16 ee4anv 1940 . . . . 5
1715, 16sylibr 204 . . . 4
18 cgsex4g.1 . . . . . 6
19182eximi 1586 . . . . 5
20192eximi 1586 . . . 4
2117, 20syl 16 . . 3
221biimprcd 217 . . . . . 6
2322ancld 537 . . . . 5
24232eximdv 1634 . . . 4
25242eximdv 1634 . . 3
2621, 25syl5com 28 . 2
274, 26impbid2 196 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359  wex 1550   wceq 1652   wcel 1725 This theorem is referenced by:  copsex4g  4437  brecop  6989 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-ext 2416 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-v 2950
 Copyright terms: Public domain W3C validator