Theorem reximdva 2608

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
reximdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
reximdva	|- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem reximdva

Step	Hyp	Ref	Expression
1		reximdva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
2	1	ex 115	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2606	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2176   E.wrex 2485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  reximddv  2609  reximddv2  2611  dffo4  5728  ctm  7211  ctssdclemn0  7212  ctssdccl  7213  ctssdc  7215  prarloclemarch  7531  appdivnq  7676  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemloc  7720  archpr  7756  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemopu  7761  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  archrecpr  7777  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemopu  7784  caucvgprlemladdfu  7790  caucvgprlemlim  7794  caucvgprprlemml  7807  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemexbt  7819  caucvgprprlemlim  7824  suplocexprlemmu  7831  suplocexprlemru  7832  suplocexprlemlub  7837  archsr  7895  suplocsrlemb  7919  suplocsrlempr  7920  cnegexlem2  8248  bndndx  9294  elpq  9770  qbtwnxr  10400  expnbnd  10808  expnlbnd2  10810  caucvgre  11292  cvg1nlemres  11296  r19.29uz  11303  resqrexlemglsq  11333  resqrexlemga  11334  cau3lem  11425  qdenre  11513  2clim  11612  climcn1  11619  climcn2  11620  climsqz  11646  climsqz2  11647  climcau  11658  divcnv  11808  divalglemex  12233  dvdsbnd  12277  bezoutlemzz  12323  bezoutlemaz  12324  bezoutlembz  12325  bezoutlembi  12326  lcmgcdlem  12399  divgcdcoprmex  12424  exprmfct  12460  prmdvdsfz  12461  pclemub  12610  pc2dvds  12653  pcprmpw  12657  dvdsprmpweqle  12660  infpnlem2  12683  prmunb  12685  ennnfonelemhom  12786  ctinf  12801  sgrpidmndm  13252  grpinveu  13370  dfgrp3mlem  13430  ringadd2  13789  znunit  14421  cnpnei  14691  txlm  14751  metequiv2  14968  metrest  14978  mulc1cncf  15061  cncfco  15063  dedekindeulemlu  15093  suplociccreex  15096  dedekindicclemlu  15102  ivthinc  15115  cnplimcim  15139  cnplimclemr  15141  limccnpcntop  15147  limccoap  15150  elply2  15207  subctctexmid  15937