Theorem reximdva 2652

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  reximddv  2653  reximddv2  2655  dffo4  5847  ctm  7439  ctssdclemn0  7440  ctssdccl  7441  ctssdc  7443  prarloclemarch  7775  appdivnq  7920  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemloc  7964  archpr  8000  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  archrecpr  8021  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemladdfu  8034  caucvgprlemlim  8038  caucvgprprlemml  8051  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemexbt  8063  caucvgprprlemlim  8068  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemlub  8081  archsr  8139  suplocsrlemb  8163  suplocsrlempr  8164  cnegexlem2  8492  bndndx  9541  elpq  10028  qbtwnxr  10670  expnbnd  11079  expnlbnd2  11081  caucvgre  11725  cvg1nlemres  11729  r19.29uz  11736  resqrexlemglsq  11766  resqrexlemga  11767  cau3lem  11858  qdenre  11946  2clim  12045  climcn1  12052  climcn2  12053  climsqz  12079  climsqz2  12080  climcau  12091  divcnv  12242  divalglemex  12667  dvdsbnd  12711  bezoutlemzz  12757  bezoutlemaz  12758  bezoutlembz  12759  bezoutlembi  12760  lcmgcdlem  12833  divgcdcoprmex  12858  exprmfct  12894  prmdvdsfz  12895  pclemub  13044  pc2dvds  13087  pcprmpw  13091  dvdsprmpweqle  13094  infpnlem2  13117  prmunb  13119  ennnfonelemhom  13284  ctinf  13299  sgrpidmndm  13710  grpinveu  13820  dfgrp3mlem  13880  ringadd2  14305  znunit  14966  cnpnei  15243  txlm  15303  metequiv2  15520  metrest  15530  mulc1cncf  15613  cncfco  15615  dedekindeulemlu  15645  suplociccreex  15648  dedekindicclemlu  15654  ivthinc  15667  cnplimcim  15691  cnplimclemr  15693  limccnpcntop  15699  limccoap  15702  elply2  15759  clwwlkn1loopb  16575  subctctexmid  16944