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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   E.wrex 2529

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  reximddv  2653  reximddv2  2655  dffo4  5856  ctm  7449  ctssdclemn0  7450  ctssdccl  7451  ctssdc  7453  prarloclemarch  7785  appdivnq  7930  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  archrecpr  8031  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemladdfu  8044  caucvgprlemlim  8048  caucvgprprlemml  8061  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemexbt  8073  caucvgprprlemlim  8078  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemlub  8091  archsr  8149  suplocsrlemb  8173  suplocsrlempr  8174  cnegexlem2  8502  bndndx  9562  elpq  10049  qbtwnxr  10692  expnbnd  11101  expnlbnd2  11103  caucvgre  11747  cvg1nlemres  11751  r19.29uz  11758  resqrexlemglsq  11788  resqrexlemga  11789  cau3lem  11880  qdenre  11968  2clim  12067  climcn1  12074  climcn2  12075  climsqz  12101  climsqz2  12102  climcau  12113  divcnv  12264  divalglemex  12689  dvdsbnd  12733  bezoutlemzz  12779  bezoutlemaz  12780  bezoutlembz  12781  bezoutlembi  12782  lcmgcdlem  12855  divgcdcoprmex  12880  exprmfct  12916  prmdvdsfz  12917  pclemub  13066  pc2dvds  13109  pcprmpw  13113  dvdsprmpweqle  13116  infpnlem2  13139  prmunb  13141  ennnfonelemhom  13306  ctinf  13321  sgrpidmndm  13733  grpinveu  13843  dfgrp3mlem  13903  ringadd2  14332  znunit  14994  cnpnei  15320  txlm  15380  metequiv2  15597  metrest  15607  mulc1cncf  15690  cncfco  15692  dedekindeulemlu  15722  suplociccreex  15725  dedekindicclemlu  15731  ivthinc  15744  cnplimcim  15768  cnplimclemr  15770  limccnpcntop  15776  limccoap  15779  elply2  15836  clwwlkn1loopb  16661  subctctexmid  17030