Theorem reximdva 2599

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  reximddv  2600  reximddv2  2602  dffo4  5713  ctm  7184  ctssdclemn0  7185  ctssdccl  7186  ctssdc  7188  prarloclemarch  7504  appdivnq  7649  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemloc  7693  archpr  7729  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemopu  7734  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  archrecpr  7750  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemopu  7757  caucvgprlemladdfu  7763  caucvgprlemlim  7767  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemopu  7785  caucvgprprlemexbt  7792  caucvgprprlemlim  7797  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemlub  7810  archsr  7868  suplocsrlemb  7892  suplocsrlempr  7893  cnegexlem2  8221  bndndx  9267  elpq  9742  qbtwnxr  10366  expnbnd  10774  expnlbnd2  10776  caucvgre  11165  cvg1nlemres  11169  r19.29uz  11176  resqrexlemglsq  11206  resqrexlemga  11207  cau3lem  11298  qdenre  11386  2clim  11485  climcn1  11492  climcn2  11493  climsqz  11519  climsqz2  11520  climcau  11531  divcnv  11681  divalglemex  12106  dvdsbnd  12150  bezoutlemzz  12196  bezoutlemaz  12197  bezoutlembz  12198  bezoutlembi  12199  lcmgcdlem  12272  divgcdcoprmex  12297  exprmfct  12333  prmdvdsfz  12334  pclemub  12483  pc2dvds  12526  pcprmpw  12530  dvdsprmpweqle  12533  infpnlem2  12556  prmunb  12558  ennnfonelemhom  12659  ctinf  12674  sgrpidmndm  13124  grpinveu  13242  dfgrp3mlem  13302  ringadd2  13661  znunit  14293  cnpnei  14563  txlm  14623  metequiv2  14840  metrest  14850  mulc1cncf  14933  cncfco  14935  dedekindeulemlu  14965  suplociccreex  14968  dedekindicclemlu  14974  ivthinc  14987  cnplimcim  15011  cnplimclemr  15013  limccnpcntop  15019  limccoap  15022  elply2  15079  subctctexmid  15755