Theorem ralimdva 2441

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
ralimdva	|- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralimdva

Step	Hyp	Ref	Expression
1		nfv 1466	. 2 |- F/ x ph
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	ralimdaa 2440	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   A.wral 2359

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 1381  ax-gen 1383  ax-4 1445  ax-17 1464

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364

This theorem is referenced by:  ralimdv  2442  f1mpt  5542  isores3  5586  caofrss  5871  caoftrn  5872  tfrlemibxssdm  6084  tfr1onlembxssdm  6100  tfrcllembxssdm  6113  tfrcl  6121  exmidomniim  6787  caucvgsrlemoffcau  7333  caucvgsrlemoffres  7335  indstr  9071  caucvgre  10402  rexuz3  10411  resqrexlemgt0  10441  resqrexlemglsq  10443  cau3lem  10535  rexanre  10641  rexico  10642  2clim  10676  climcn1  10684  climcn2  10685  subcn2  10687  climsqz  10710  climsqz2  10711  climcvg1nlem  10725  bezoutlemaz  11257  bezoutlembz  11258  bezoutlembi  11259  rescncf  11520  cncfco  11530