Theorem reximdva 2634

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  reximddv  2635  reximddv2  2637  dffo4  5795  ctm  7307  ctssdclemn0  7308  ctssdccl  7309  ctssdc  7311  prarloclemarch  7637  appdivnq  7782  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemloc  7826  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemopu  7867  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  archrecpr  7883  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemopu  7890  caucvgprlemladdfu  7896  caucvgprlemlim  7900  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemexbt  7925  caucvgprprlemlim  7930  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemlub  7943  archsr  8001  suplocsrlemb  8025  suplocsrlempr  8026  cnegexlem2  8354  bndndx  9400  elpq  9882  qbtwnxr  10516  expnbnd  10924  expnlbnd2  10926  caucvgre  11541  cvg1nlemres  11545  r19.29uz  11552  resqrexlemglsq  11582  resqrexlemga  11583  cau3lem  11674  qdenre  11762  2clim  11861  climcn1  11868  climcn2  11869  climsqz  11895  climsqz2  11896  climcau  11907  divcnv  12057  divalglemex  12482  dvdsbnd  12526  bezoutlemzz  12572  bezoutlemaz  12573  bezoutlembz  12574  bezoutlembi  12575  lcmgcdlem  12648  divgcdcoprmex  12673  exprmfct  12709  prmdvdsfz  12710  pclemub  12859  pc2dvds  12902  pcprmpw  12906  dvdsprmpweqle  12909  infpnlem2  12932  prmunb  12934  ennnfonelemhom  13035  ctinf  13050  sgrpidmndm  13502  grpinveu  13620  dfgrp3mlem  13680  ringadd2  14039  znunit  14672  cnpnei  14942  txlm  15002  metequiv2  15219  metrest  15229  mulc1cncf  15312  cncfco  15314  dedekindeulemlu  15344  suplociccreex  15347  dedekindicclemlu  15353  ivthinc  15366  cnplimcim  15390  cnplimclemr  15392  limccnpcntop  15398  limccoap  15401  elply2  15458  clwwlkn1loopb  16270  subctctexmid  16601