Theorem reximdva 2463

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 113	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2461	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1433   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353  df-rex 2354

This theorem is referenced by:  reximddv  2464  reximddv2  2465  dffo4  5336  prarloclemarch  6608  appdivnq  6753  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  archpr  6833  cauappcvgprlemm  6835  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  archrecpr  6854  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemladdfu  6867  caucvgprlemlim  6871  caucvgprprlemml  6884  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemexbt  6896  caucvgprprlemlim  6901  archsr  6958  cnegexlem2  7284  bndndx  8287  qbtwnxr  9266  expnbnd  9596  expnlbnd2  9598  caucvgre  9867  cvg1nlemres  9871  r19.29uz  9878  resqrexlemglsq  9908  resqrexlemga  9909  cau3lem  10000  qdenre  10088  2clim  10140  climcn1  10147  climcn2  10148  climsqz  10173  climsqz2  10174  climcau  10184  divalglemex  10322  dvdsbnd  10348  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlembi  10394  lcmgcdlem  10459  divgcdcoprmex  10484  exprmfct  10519  prmdvdsfz  10520