Theorem reximdva 2635

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

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

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 2516  df-rex 2517

This theorem is referenced by:  reximddv  2636  reximddv2  2638  dffo4  5803  ctm  7351  ctssdclemn0  7352  ctssdccl  7353  ctssdc  7355  prarloclemarch  7681  appdivnq  7826  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemloc  7870  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  archrecpr  7927  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemladdfu  7940  caucvgprlemlim  7944  caucvgprprlemml  7957  caucvgprprlemopl  7960  caucvgprprlemlol  7961  caucvgprprlemopu  7962  caucvgprprlemexbt  7969  caucvgprprlemlim  7974  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemlub  7987  archsr  8045  suplocsrlemb  8069  suplocsrlempr  8070  cnegexlem2  8398  bndndx  9444  elpq  9928  qbtwnxr  10563  expnbnd  10971  expnlbnd2  10973  caucvgre  11604  cvg1nlemres  11608  r19.29uz  11615  resqrexlemglsq  11645  resqrexlemga  11646  cau3lem  11737  qdenre  11825  2clim  11924  climcn1  11931  climcn2  11932  climsqz  11958  climsqz2  11959  climcau  11970  divcnv  12121  divalglemex  12546  dvdsbnd  12590  bezoutlemzz  12636  bezoutlemaz  12637  bezoutlembz  12638  bezoutlembi  12639  lcmgcdlem  12712  divgcdcoprmex  12737  exprmfct  12773  prmdvdsfz  12774  pclemub  12923  pc2dvds  12966  pcprmpw  12970  dvdsprmpweqle  12973  infpnlem2  12996  prmunb  12998  ennnfonelemhom  13099  ctinf  13114  sgrpidmndm  13566  grpinveu  13684  dfgrp3mlem  13744  ringadd2  14104  znunit  14738  cnpnei  15013  txlm  15073  metequiv2  15290  metrest  15300  mulc1cncf  15383  cncfco  15385  dedekindeulemlu  15415  suplociccreex  15418  dedekindicclemlu  15424  ivthinc  15437  cnplimcim  15461  cnplimclemr  15463  limccnpcntop  15469  limccoap  15472  elply2  15529  clwwlkn1loopb  16344  subctctexmid  16705