Theorem reximdva 2579

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  reximddv  2580  reximddv2  2582  dffo4  5665  ctm  7108  ctssdclemn0  7109  ctssdccl  7110  ctssdc  7112  prarloclemarch  7417  appdivnq  7562  ltexprlemm  7599  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemloc  7606  archpr  7642  cauappcvgprlemm  7644  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemopu  7647  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  archrecpr  7663  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemopu  7670  caucvgprlemladdfu  7676  caucvgprlemlim  7680  caucvgprprlemml  7693  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemexbt  7705  caucvgprprlemlim  7710  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemlub  7723  archsr  7781  suplocsrlemb  7805  suplocsrlempr  7806  cnegexlem2  8133  bndndx  9175  elpq  9648  qbtwnxr  10258  expnbnd  10644  expnlbnd2  10646  caucvgre  10990  cvg1nlemres  10994  r19.29uz  11001  resqrexlemglsq  11031  resqrexlemga  11032  cau3lem  11123  qdenre  11211  2clim  11309  climcn1  11316  climcn2  11317  climsqz  11343  climsqz2  11344  climcau  11355  divcnv  11505  divalglemex  11927  dvdsbnd  11957  bezoutlemzz  12003  bezoutlemaz  12004  bezoutlembz  12005  bezoutlembi  12006  lcmgcdlem  12077  divgcdcoprmex  12102  exprmfct  12138  prmdvdsfz  12139  pclemub  12287  pc2dvds  12329  pcprmpw  12333  dvdsprmpweqle  12336  infpnlem2  12358  prmunb  12360  ennnfonelemhom  12416  ctinf  12431  sgrpidmndm  12821  grpinveu  12911  dfgrp3mlem  12968  ringadd2  13210  cnpnei  13722  txlm  13782  metequiv2  13999  metrest  14009  mulc1cncf  14079  cncfco  14081  dedekindeulemlu  14102  suplociccreex  14105  dedekindicclemlu  14111  ivthinc  14124  cnplimcim  14139  cnplimclemr  14141  limccnpcntop  14147  limccoap  14150  subctctexmid  14753