Theorem reximdva 2644

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2525  df-rex 2526

This theorem is referenced by:  reximddv  2645  reximddv2  2647  dffo4  5825  ctm  7400  ctssdclemn0  7401  ctssdccl  7402  ctssdc  7404  prarloclemarch  7733  appdivnq  7878  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemloc  7922  archpr  7958  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemopu  7963  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  archrecpr  7979  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemopu  7986  caucvgprlemladdfu  7992  caucvgprlemlim  7996  caucvgprprlemml  8009  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemexbt  8021  caucvgprprlemlim  8026  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemlub  8039  archsr  8097  suplocsrlemb  8121  suplocsrlempr  8122  cnegexlem2  8449  bndndx  9495  elpq  9981  qbtwnxr  10617  expnbnd  11025  expnlbnd2  11027  caucvgre  11666  cvg1nlemres  11670  r19.29uz  11677  resqrexlemglsq  11707  resqrexlemga  11708  cau3lem  11799  qdenre  11887  2clim  11986  climcn1  11993  climcn2  11994  climsqz  12020  climsqz2  12021  climcau  12032  divcnv  12183  divalglemex  12608  dvdsbnd  12652  bezoutlemzz  12698  bezoutlemaz  12699  bezoutlembz  12700  bezoutlembi  12701  lcmgcdlem  12774  divgcdcoprmex  12799  exprmfct  12835  prmdvdsfz  12836  pclemub  12985  pc2dvds  13028  pcprmpw  13032  dvdsprmpweqle  13035  infpnlem2  13058  prmunb  13060  ennnfonelemhom  13166  ctinf  13181  sgrpidmndm  13633  grpinveu  13751  dfgrp3mlem  13811  ringadd2  14171  znunit  14807  cnpnei  15084  txlm  15144  metequiv2  15361  metrest  15371  mulc1cncf  15454  cncfco  15456  dedekindeulemlu  15486  suplociccreex  15489  dedekindicclemlu  15495  ivthinc  15508  cnplimcim  15532  cnplimclemr  15534  limccnpcntop  15540  limccoap  15543  elply2  15600  clwwlkn1loopb  16415  subctctexmid  16774