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  7450  ctssdclemn0  7451  ctssdccl  7452  ctssdc  7454  prarloclemarch  7786  appdivnq  7931  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  archrecpr  8032  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemladdfu  8045  caucvgprlemlim  8049  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemopu  8067  caucvgprprlemexbt  8074  caucvgprprlemlim  8079  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemlub  8092  archsr  8150  suplocsrlemb  8174  suplocsrlempr  8175  cnegexlem2  8504  bndndx  9567  elpq  10060  qbtwnxr  10703  expnbnd  11116  expnlbnd2  11118  caucvgre  11763  cvg1nlemres  11767  r19.29uz  11774  resqrexlemglsq  11804  resqrexlemga  11805  cau3lem  11897  qdenre  11985  2clim  12086  climcn1  12093  climcn2  12094  climsqz  12120  climsqz2  12121  climcau  12132  divcnv  12283  divalglemex  12708  dvdsbnd  12752  bezoutlemzz  12798  bezoutlemaz  12799  bezoutlembz  12800  bezoutlembi  12801  lcmgcdlem  12874  divgcdcoprmex  12899  exprmfct  12936  prmdvdsfz  12937  pclemub  13089  pc2dvds  13132  pcprmpw  13136  dvdsprmpweqle  13139  infpnlem2  13162  prmunb  13164  ennnfonelemhom  13358  ctinf  13373  sgrpidmndm  13786  grpinveu  13896  dfgrp3mlem  13956  ringadd2  14416  znunit  15078  cnpnei  15411  txlm  15471  metequiv2  15688  metrest  15698  mulc1cncf  15781  cncfco  15783  dedekindeulemlu  15813  suplociccreex  15816  dedekindicclemlu  15822  ivthinc  15835  cnplimcim  15859  cnplimclemr  15861  limccnpcntop  15867  limccoap  15870  elply2  15927  clwwlkn1loopb  16827  subctctexmid  17196