Theorem ralimdv 2500

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

Hypothesis

Ref	Expression
ralimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
ralimdv	|- ( 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 ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	adantr 274	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2499	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1480   A.wral 2416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  poss  4220  sess1  4259  sess2  4260  riinint  4800  dffo4  5568  dffo5  5569  isoini2  5720  rdgivallem  6278  iinerm  6501  xpf1o  6738  resqrexlemgt0  10792  cau3lem  10886  caubnd2  10889  climshftlemg  11071  climcau  11116  climcaucn  11120  serf0  11121  modfsummodlemstep  11226  bezoutlemmain  11686  ctinf  11943  strsetsid  11992  fiinbas  12216  baspartn  12217  lmtopcnp  12419  rescncf  12737  limcresi  12804