Theorem ralimdv 2545

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  poss  4298  sess1  4337  sess2  4338  riinint  4888  dffo4  5664  dffo5  5665  isoini2  5819  rdgivallem  6381  iinerm  6606  xpf1o  6843  exmidontriimlem3  7221  exmidontriim  7223  resqrexlemgt0  11028  cau3lem  11122  caubnd2  11125  climshftlemg  11309  climcau  11354  climcaucn  11358  serf0  11359  modfsummodlemstep  11464  bezoutlemmain  11998  ctinf  12430  strsetsid  12494  imasaddfnlemg  12734  fiinbas  13485  baspartn  13486  lmtopcnp  13686  rescncf  14004  limcresi  14071