Theorem cgsex4g 3144

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:   ,,,,   ,,,,   ,,,,   ,,,,   ,,,,

Proof of Theorem cgsex4g

Step	Hyp	Ref	Expression
1		cgsex4g.2	. . . . 5
2	1	biimpa 484	. . . 4
3	2	exlimivv 1723	. . 3
4	3	exlimivv 1723	. 2
5		elisset 3120	. . . . . . . 8
6		elisset 3120	. . . . . . . 8
7	5, 6	anim12i 566	. . . . . . 7
8		eeanv 1988	. . . . . . 7
9	7, 8	sylibr 212	. . . . . 6
10		elisset 3120	. . . . . . . 8
11		elisset 3120	. . . . . . . 8
12	10, 11	anim12i 566	. . . . . . 7
13		eeanv 1988	. . . . . . 7
14	12, 13	sylibr 212	. . . . . 6
15	9, 14	anim12i 566	. . . . 5
16		ee4anv 1990	. . . . 5
17	15, 16	sylibr 212	. . . 4
18		cgsex4g.1	. . . . . 6
19	18	2eximi 1657	. . . . 5
20	19	2eximi 1657	. . . 4
21	17, 20	syl 16	. . 3
22	1	biimprcd 225	. . . . . 6
23	22	ancld 553	. . . . 5
24	23	2eximdv 1712	. . . 4
25	24	2eximdv 1712	. . 3
26	21, 25	syl5com 30	. 2
27	4, 26	impbid2 204	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818

This theorem is referenced by:  copsex4g  4741  brecop  7423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111