Theorem ralimdv 2538

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 2537	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 2141   A.wral 2448

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  poss  4283  sess1  4322  sess2  4323  riinint  4872  dffo4  5644  dffo5  5645  isoini2  5798  rdgivallem  6360  iinerm  6585  xpf1o  6822  exmidontriimlem3  7200  exmidontriim  7202  resqrexlemgt0  10984  cau3lem  11078  caubnd2  11081  climshftlemg  11265  climcau  11310  climcaucn  11314  serf0  11315  modfsummodlemstep  11420  bezoutlemmain  11953  ctinf  12385  strsetsid  12449  fiinbas  12841  baspartn  12842  lmtopcnp  13044  rescncf  13362  limcresi  13429