Theorem reximdva 2635

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  reximddv  2636  reximddv2  2638  dffo4  5803  ctm  7368  ctssdclemn0  7369  ctssdccl  7370  ctssdc  7372  prarloclemarch  7698  appdivnq  7843  ltexprlemm  7880  ltexprlemopl  7881  ltexprlemopu  7883  ltexprlemloc  7887  archpr  7923  cauappcvgprlemm  7925  cauappcvgprlemopl  7926  cauappcvgprlemlol  7927  cauappcvgprlemopu  7928  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  archrecpr  7944  caucvgprlemm  7948  caucvgprlemopl  7949  caucvgprlemlol  7950  caucvgprlemopu  7951  caucvgprlemladdfu  7957  caucvgprlemlim  7961  caucvgprprlemml  7974  caucvgprprlemopl  7977  caucvgprprlemlol  7978  caucvgprprlemopu  7979  caucvgprprlemexbt  7986  caucvgprprlemlim  7991  suplocexprlemmu  7998  suplocexprlemru  7999  suplocexprlemlub  8004  archsr  8062  suplocsrlemb  8086  suplocsrlempr  8087  cnegexlem2  8414  bndndx  9460  elpq  9944  qbtwnxr  10580  expnbnd  10988  expnlbnd2  10990  caucvgre  11621  cvg1nlemres  11625  r19.29uz  11632  resqrexlemglsq  11662  resqrexlemga  11663  cau3lem  11754  qdenre  11842  2clim  11941  climcn1  11948  climcn2  11949  climsqz  11975  climsqz2  11976  climcau  11987  divcnv  12138  divalglemex  12563  dvdsbnd  12607  bezoutlemzz  12653  bezoutlemaz  12654  bezoutlembz  12655  bezoutlembi  12656  lcmgcdlem  12729  divgcdcoprmex  12754  exprmfct  12790  prmdvdsfz  12791  pclemub  12940  pc2dvds  12983  pcprmpw  12987  dvdsprmpweqle  12990  infpnlem2  13013  prmunb  13015  ennnfonelemhom  13116  ctinf  13131  sgrpidmndm  13583  grpinveu  13701  dfgrp3mlem  13761  ringadd2  14121  znunit  14755  cnpnei  15030  txlm  15090  metequiv2  15307  metrest  15317  mulc1cncf  15400  cncfco  15402  dedekindeulemlu  15432  suplociccreex  15435  dedekindicclemlu  15441  ivthinc  15454  cnplimcim  15478  cnplimclemr  15480  limccnpcntop  15486  limccoap  15489  elply2  15546  clwwlkn1loopb  16361  subctctexmid  16722