Theorem ralimdv 2472

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 272	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2471	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1461   A.wral 2388

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

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-ral 2393

This theorem is referenced by:  poss  4178  sess1  4217  sess2  4218  riinint  4756  dffo4  5520  dffo5  5521  isoini2  5672  rdgivallem  6230  iinerm  6453  xpf1o  6689  resqrexlemgt0  10678  cau3lem  10772  caubnd2  10775  climshftlemg  10957  climcau  11002  climcaucn  11006  serf0  11007  modfsummodlemstep  11112  bezoutlemmain  11526  ctinf  11782  strsetsid  11829  fiinbas  12053  baspartn  12054  lmtopcnp  12255  rescncf  12548  limcresi  12585