Theorem reximdva 2415

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

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1390  E.wrex 2301

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306

This theorem is referenced by:  dffo4  5258  prarloclemarch  6401  appdivnq  6544  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemladdfu  6648  caucvgprlemlim  6652  archsr  6708  cnegexlem2  6984  bndndx  7956  expnbnd  9025  expnlbnd2  9027