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  5785  ctm  7287  ctssdclemn0  7288  ctssdccl  7289  ctssdc  7291  prarloclemarch  7616  appdivnq  7761  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemloc  7805  archpr  7841  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemopu  7846  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  archrecpr  7862  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemopu  7869  caucvgprlemladdfu  7875  caucvgprlemlim  7879  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemexbt  7904  caucvgprprlemlim  7909  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemlub  7922  archsr  7980  suplocsrlemb  8004  suplocsrlempr  8005  cnegexlem2  8333  bndndx  9379  elpq  9856  qbtwnxr  10489  expnbnd  10897  expnlbnd2  10899  caucvgre  11508  cvg1nlemres  11512  r19.29uz  11519  resqrexlemglsq  11549  resqrexlemga  11550  cau3lem  11641  qdenre  11729  2clim  11828  climcn1  11835  climcn2  11836  climsqz  11862  climsqz2  11863  climcau  11874  divcnv  12024  divalglemex  12449  dvdsbnd  12493  bezoutlemzz  12539  bezoutlemaz  12540  bezoutlembz  12541  bezoutlembi  12542  lcmgcdlem  12615  divgcdcoprmex  12640  exprmfct  12676  prmdvdsfz  12677  pclemub  12826  pc2dvds  12869  pcprmpw  12873  dvdsprmpweqle  12876  infpnlem2  12899  prmunb  12901  ennnfonelemhom  13002  ctinf  13017  sgrpidmndm  13469  grpinveu  13587  dfgrp3mlem  13647  ringadd2  14006  znunit  14639  cnpnei  14909  txlm  14969  metequiv2  15186  metrest  15196  mulc1cncf  15279  cncfco  15281  dedekindeulemlu  15311  suplociccreex  15314  dedekindicclemlu  15320  ivthinc  15333  cnplimcim  15357  cnplimclemr  15359  limccnpcntop  15365  limccoap  15368  elply2  15425  clwwlkn1loopb  16162  subctctexmid  16453