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  8503  bndndx  9566  elpq  10059  qbtwnxr  10702  expnbnd  11114  expnlbnd2  11116  caucvgre  11761  cvg1nlemres  11765  r19.29uz  11772  resqrexlemglsq  11802  resqrexlemga  11803  cau3lem  11895  qdenre  11983  2clim  12083  climcn1  12090  climcn2  12091  climsqz  12117  climsqz2  12118  climcau  12129  divcnv  12280  divalglemex  12705  dvdsbnd  12749  bezoutlemzz  12795  bezoutlemaz  12796  bezoutlembz  12797  bezoutlembi  12798  lcmgcdlem  12871  divgcdcoprmex  12896  exprmfct  12933  prmdvdsfz  12934  pclemub  13086  pc2dvds  13129  pcprmpw  13133  dvdsprmpweqle  13136  infpnlem2  13159  prmunb  13161  ennnfonelemhom  13355  ctinf  13370  sgrpidmndm  13782  grpinveu  13892  dfgrp3mlem  13952  ringadd2  14381  znunit  15043  cnpnei  15369  txlm  15429  metequiv2  15646  metrest  15656  mulc1cncf  15739  cncfco  15741  dedekindeulemlu  15771  suplociccreex  15774  dedekindicclemlu  15780  ivthinc  15793  cnplimcim  15817  cnplimclemr  15819  limccnpcntop  15825  limccoap  15828  elply2  15885  clwwlkn1loopb  16759  subctctexmid  17128