Theorem reximdva 2634

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 2632	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  reximddv  2635  reximddv2  2637  dffo4  5795  ctm  7308  ctssdclemn0  7309  ctssdccl  7310  ctssdc  7312  prarloclemarch  7638  appdivnq  7783  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  archrecpr  7884  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemladdfu  7897  caucvgprlemlim  7901  caucvgprprlemml  7914  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  caucvgprprlemlim  7931  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemlub  7944  archsr  8002  suplocsrlemb  8026  suplocsrlempr  8027  cnegexlem2  8355  bndndx  9401  elpq  9883  qbtwnxr  10518  expnbnd  10926  expnlbnd2  10928  caucvgre  11559  cvg1nlemres  11563  r19.29uz  11570  resqrexlemglsq  11600  resqrexlemga  11601  cau3lem  11692  qdenre  11780  2clim  11879  climcn1  11886  climcn2  11887  climsqz  11913  climsqz2  11914  climcau  11925  divcnv  12076  divalglemex  12501  dvdsbnd  12545  bezoutlemzz  12591  bezoutlemaz  12592  bezoutlembz  12593  bezoutlembi  12594  lcmgcdlem  12667  divgcdcoprmex  12692  exprmfct  12728  prmdvdsfz  12729  pclemub  12878  pc2dvds  12921  pcprmpw  12925  dvdsprmpweqle  12928  infpnlem2  12951  prmunb  12953  ennnfonelemhom  13054  ctinf  13069  sgrpidmndm  13521  grpinveu  13639  dfgrp3mlem  13699  ringadd2  14059  znunit  14692  cnpnei  14962  txlm  15022  metequiv2  15239  metrest  15249  mulc1cncf  15332  cncfco  15334  dedekindeulemlu  15364  suplociccreex  15367  dedekindicclemlu  15373  ivthinc  15386  cnplimcim  15410  cnplimclemr  15412  limccnpcntop  15418  limccoap  15421  elply2  15478  clwwlkn1loopb  16290  subctctexmid  16652