Theorem ralimdva 2387

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 1421	. 2 |- F/ x ph
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	ralimdaa 2386	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 97   e. wcel 1393   A.wral 2306

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-4 1400  ax-17 1419

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

This theorem is referenced by:  ralimdv  2388  f1mpt  5410  isores3  5455  caofrss  5735  caoftrn  5736  tfrlemibxssdm  5941  rdgon  5973  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  indstr  8536  caucvgre  9580  rexuz3  9588  resqrexlemgt0  9618  resqrexlemglsq  9620  cau3lem  9710  2clim  9822  climcn1  9829  climcn2  9830  subcn2  9832  climsqz  9855  climsqz2  9856  climcvg1nlem  9868