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  5710  ctm  7175  ctssdclemn0  7176  ctssdccl  7177  ctssdc  7179  prarloclemarch  7485  appdivnq  7630  ltexprlemm  7667  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemloc  7674  archpr  7710  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemopu  7715  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  archrecpr  7731  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemopu  7738  caucvgprlemladdfu  7744  caucvgprlemlim  7748  caucvgprprlemml  7761  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemexbt  7773  caucvgprprlemlim  7778  suplocexprlemmu  7785  suplocexprlemru  7786  suplocexprlemlub  7791  archsr  7849  suplocsrlemb  7873  suplocsrlempr  7874  cnegexlem2  8202  bndndx  9248  elpq  9723  qbtwnxr  10347  expnbnd  10755  expnlbnd2  10757  caucvgre  11146  cvg1nlemres  11150  r19.29uz  11157  resqrexlemglsq  11187  resqrexlemga  11188  cau3lem  11279  qdenre  11367  2clim  11466  climcn1  11473  climcn2  11474  climsqz  11500  climsqz2  11501  climcau  11512  divcnv  11662  divalglemex  12087  dvdsbnd  12123  bezoutlemzz  12169  bezoutlemaz  12170  bezoutlembz  12171  bezoutlembi  12172  lcmgcdlem  12245  divgcdcoprmex  12270  exprmfct  12306  prmdvdsfz  12307  pclemub  12456  pc2dvds  12499  pcprmpw  12503  dvdsprmpweqle  12506  infpnlem2  12529  prmunb  12531  ennnfonelemhom  12632  ctinf  12647  sgrpidmndm  13061  grpinveu  13170  dfgrp3mlem  13230  ringadd2  13583  znunit  14215  cnpnei  14455  txlm  14515  metequiv2  14732  metrest  14742  mulc1cncf  14825  cncfco  14827  dedekindeulemlu  14857  suplociccreex  14860  dedekindicclemlu  14866  ivthinc  14879  cnplimcim  14903  cnplimclemr  14905  limccnpcntop  14911  limccoap  14914  elply2  14971  subctctexmid  15645