Theorem reximdva 2610

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491  df-rex 2492

This theorem is referenced by:  reximddv  2611  reximddv2  2613  dffo4  5751  ctm  7237  ctssdclemn0  7238  ctssdccl  7239  ctssdc  7241  prarloclemarch  7566  appdivnq  7711  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemopu  7751  ltexprlemloc  7755  archpr  7791  cauappcvgprlemm  7793  cauappcvgprlemopl  7794  cauappcvgprlemlol  7795  cauappcvgprlemopu  7796  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  archrecpr  7812  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemopu  7819  caucvgprlemladdfu  7825  caucvgprlemlim  7829  caucvgprprlemml  7842  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemexbt  7854  caucvgprprlemlim  7859  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemlub  7872  archsr  7930  suplocsrlemb  7954  suplocsrlempr  7955  cnegexlem2  8283  bndndx  9329  elpq  9805  qbtwnxr  10437  expnbnd  10845  expnlbnd2  10847  caucvgre  11407  cvg1nlemres  11411  r19.29uz  11418  resqrexlemglsq  11448  resqrexlemga  11449  cau3lem  11540  qdenre  11628  2clim  11727  climcn1  11734  climcn2  11735  climsqz  11761  climsqz2  11762  climcau  11773  divcnv  11923  divalglemex  12348  dvdsbnd  12392  bezoutlemzz  12438  bezoutlemaz  12439  bezoutlembz  12440  bezoutlembi  12441  lcmgcdlem  12514  divgcdcoprmex  12539  exprmfct  12575  prmdvdsfz  12576  pclemub  12725  pc2dvds  12768  pcprmpw  12772  dvdsprmpweqle  12775  infpnlem2  12798  prmunb  12800  ennnfonelemhom  12901  ctinf  12916  sgrpidmndm  13367  grpinveu  13485  dfgrp3mlem  13545  ringadd2  13904  znunit  14536  cnpnei  14806  txlm  14866  metequiv2  15083  metrest  15093  mulc1cncf  15176  cncfco  15178  dedekindeulemlu  15208  suplociccreex  15211  dedekindicclemlu  15217  ivthinc  15230  cnplimcim  15254  cnplimclemr  15256  limccnpcntop  15262  limccoap  15265  elply2  15322  subctctexmid  16139