Theorem reximdva 2608

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  reximddv  2609  reximddv2  2611  dffo4  5730  ctm  7213  ctssdclemn0  7214  ctssdccl  7215  ctssdc  7217  prarloclemarch  7533  appdivnq  7678  ltexprlemm  7715  ltexprlemopl  7716  ltexprlemopu  7718  ltexprlemloc  7722  archpr  7758  cauappcvgprlemm  7760  cauappcvgprlemopl  7761  cauappcvgprlemlol  7762  cauappcvgprlemopu  7763  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  archrecpr  7779  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemopu  7786  caucvgprlemladdfu  7792  caucvgprlemlim  7796  caucvgprprlemml  7809  caucvgprprlemopl  7812  caucvgprprlemlol  7813  caucvgprprlemopu  7814  caucvgprprlemexbt  7821  caucvgprprlemlim  7826  suplocexprlemmu  7833  suplocexprlemru  7834  suplocexprlemlub  7839  archsr  7897  suplocsrlemb  7921  suplocsrlempr  7922  cnegexlem2  8250  bndndx  9296  elpq  9772  qbtwnxr  10402  expnbnd  10810  expnlbnd2  10812  caucvgre  11325  cvg1nlemres  11329  r19.29uz  11336  resqrexlemglsq  11366  resqrexlemga  11367  cau3lem  11458  qdenre  11546  2clim  11645  climcn1  11652  climcn2  11653  climsqz  11679  climsqz2  11680  climcau  11691  divcnv  11841  divalglemex  12266  dvdsbnd  12310  bezoutlemzz  12356  bezoutlemaz  12357  bezoutlembz  12358  bezoutlembi  12359  lcmgcdlem  12432  divgcdcoprmex  12457  exprmfct  12493  prmdvdsfz  12494  pclemub  12643  pc2dvds  12686  pcprmpw  12690  dvdsprmpweqle  12693  infpnlem2  12716  prmunb  12718  ennnfonelemhom  12819  ctinf  12834  sgrpidmndm  13285  grpinveu  13403  dfgrp3mlem  13463  ringadd2  13822  znunit  14454  cnpnei  14724  txlm  14784  metequiv2  15001  metrest  15011  mulc1cncf  15094  cncfco  15096  dedekindeulemlu  15126  suplociccreex  15129  dedekindicclemlu  15135  ivthinc  15148  cnplimcim  15172  cnplimclemr  15174  limccnpcntop  15180  limccoap  15183  elply2  15240  subctctexmid  15974