Theorem ralimdva 2429

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

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

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-4 1440  ax-17 1459

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

This theorem is referenced by:  ralimdv  2430  f1mpt  5431  isores3  5475  caofrss  5755  caoftrn  5756  tfrlemibxssdm  5964  rdgon  5996  caucvgsrlemoffcau  6974  caucvgsrlemoffres  6976  indstr  8681  caucvgre  9867  rexuz3  9876  resqrexlemgt0  9906  resqrexlemglsq  9908  cau3lem  10000  rexanre  10106  rexico  10107  2clim  10140  climcn1  10147  climcn2  10148  subcn2  10150  climsqz  10173  climsqz2  10174  climcvg1nlem  10186  bezoutlemaz  10392  bezoutlembz  10393  bezoutlembi  10394