Theorem reximdva 2421

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

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

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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312

This theorem is referenced by:  dffo4  5315  prarloclemarch  6516  appdivnq  6661  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemloc  6705  archpr  6741  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemopu  6746  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  archrecpr  6762  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemopu  6769  caucvgprlemladdfu  6775  caucvgprlemlim  6779  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemopu  6797  caucvgprprlemexbt  6804  caucvgprprlemlim  6809  archsr  6866  cnegexlem2  7187  bndndx  8180  expnbnd  9372  expnlbnd2  9374  caucvgre  9580  cvg1nlemres  9584  r19.29uz  9590  resqrexlemglsq  9620  resqrexlemga  9621  cau3lem  9710  qdenre  9798  2clim  9822  climcn1  9829  climcn2  9830  climsqz  9855  climsqz2  9856  climcau  9866