Theorem ceqsex2 3147

Description: Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.)

Hypotheses

Ref	Expression
ceqsex2.1
ceqsex2.2
ceqsex2.3
ceqsex2.4
ceqsex2.5
ceqsex2.6

Assertion

Ref	Expression
ceqsex2

Distinct variable groups:   ,,   ,,

Proof of Theorem ceqsex2

Step	Hyp	Ref	Expression
1		3anass 977	. . . . 5
2	1	exbii 1667	. . . 4
3		19.42v 1775	. . . 4
4	2, 3	bitri 249	. . 3
5	4	exbii 1667	. 2
6		nfv 1707	. . . . 5
7		ceqsex2.1	. . . . 5
8	6, 7	nfan 1928	. . . 4
9	8	nfex 1948	. . 3
10		ceqsex2.3	. . 3
11		ceqsex2.5	. . . . 5
12	11	anbi2d 703	. . . 4
13	12	exbidv 1714	. . 3
14	9, 10, 13	ceqsex 3145	. 2
15		ceqsex2.2	. . 3
16		ceqsex2.4	. . 3
17		ceqsex2.6	. . 3
18	15, 16, 17	ceqsex 3145	. 2
19	5, 14, 18	3bitri 271	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  E.wex 1612  F/wnf 1616  e.wcel 1818  cvv 3109

This theorem is referenced by:  ceqsex2v  3148

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-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111