Theorem reximdva 2632

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  reximddv  2633  reximddv2  2635  dffo4  5791  ctm  7299  ctssdclemn0  7300  ctssdccl  7301  ctssdc  7303  prarloclemarch  7628  appdivnq  7773  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemloc  7817  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemopu  7858  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  archrecpr  7874  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemopu  7881  caucvgprlemladdfu  7887  caucvgprlemlim  7891  caucvgprprlemml  7904  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemexbt  7916  caucvgprprlemlim  7921  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemlub  7934  archsr  7992  suplocsrlemb  8016  suplocsrlempr  8017  cnegexlem2  8345  bndndx  9391  elpq  9873  qbtwnxr  10507  expnbnd  10915  expnlbnd2  10917  caucvgre  11532  cvg1nlemres  11536  r19.29uz  11543  resqrexlemglsq  11573  resqrexlemga  11574  cau3lem  11665  qdenre  11753  2clim  11852  climcn1  11859  climcn2  11860  climsqz  11886  climsqz2  11887  climcau  11898  divcnv  12048  divalglemex  12473  dvdsbnd  12517  bezoutlemzz  12563  bezoutlemaz  12564  bezoutlembz  12565  bezoutlembi  12566  lcmgcdlem  12639  divgcdcoprmex  12664  exprmfct  12700  prmdvdsfz  12701  pclemub  12850  pc2dvds  12893  pcprmpw  12897  dvdsprmpweqle  12900  infpnlem2  12923  prmunb  12925  ennnfonelemhom  13026  ctinf  13041  sgrpidmndm  13493  grpinveu  13611  dfgrp3mlem  13671  ringadd2  14030  znunit  14663  cnpnei  14933  txlm  14993  metequiv2  15210  metrest  15220  mulc1cncf  15303  cncfco  15305  dedekindeulemlu  15335  suplociccreex  15338  dedekindicclemlu  15344  ivthinc  15357  cnplimcim  15381  cnplimclemr  15383  limccnpcntop  15389  limccoap  15392  elply2  15449  clwwlkn1loopb  16215  subctctexmid  16537