Theorem reximdva 2646

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

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

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 2527  df-rex 2528

This theorem is referenced by:  reximddv  2647  reximddv2  2649  dffo4  5830  ctm  7413  ctssdclemn0  7414  ctssdccl  7415  ctssdc  7417  prarloclemarch  7749  appdivnq  7894  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  archrecpr  7995  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemladdfu  8008  caucvgprlemlim  8012  caucvgprprlemml  8025  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemexbt  8037  caucvgprprlemlim  8042  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemlub  8055  archsr  8113  suplocsrlemb  8137  suplocsrlempr  8138  cnegexlem2  8465  bndndx  9512  elpq  9999  qbtwnxr  10641  expnbnd  11050  expnlbnd2  11052  caucvgre  11691  cvg1nlemres  11695  r19.29uz  11702  resqrexlemglsq  11732  resqrexlemga  11733  cau3lem  11824  qdenre  11912  2clim  12011  climcn1  12018  climcn2  12019  climsqz  12045  climsqz2  12046  climcau  12057  divcnv  12208  divalglemex  12633  dvdsbnd  12677  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  bezoutlembi  12726  lcmgcdlem  12799  divgcdcoprmex  12824  exprmfct  12860  prmdvdsfz  12861  pclemub  13010  pc2dvds  13053  pcprmpw  13057  dvdsprmpweqle  13060  infpnlem2  13083  prmunb  13085  ennnfonelemhom  13250  ctinf  13265  sgrpidmndm  13681  grpinveu  13793  dfgrp3mlem  13853  ringadd2  14270  znunit  14933  cnpnei  15210  txlm  15270  metequiv2  15487  metrest  15497  mulc1cncf  15580  cncfco  15582  dedekindeulemlu  15612  suplociccreex  15615  dedekindicclemlu  15621  ivthinc  15634  cnplimcim  15658  cnplimclemr  15660  limccnpcntop  15666  limccoap  15669  elply2  15726  clwwlkn1loopb  16541  subctctexmid  16900