Theorem ralimdv 2534

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

Syntax hints:   -> wi 4   e. wcel 2136   A.wral 2444

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  poss  4276  sess1  4315  sess2  4316  riinint  4865  dffo4  5633  dffo5  5634  isoini2  5787  rdgivallem  6349  iinerm  6573  xpf1o  6810  exmidontriimlem3  7179  exmidontriim  7181  resqrexlemgt0  10962  cau3lem  11056  caubnd2  11059  climshftlemg  11243  climcau  11288  climcaucn  11292  serf0  11293  modfsummodlemstep  11398  bezoutlemmain  11931  ctinf  12363  strsetsid  12427  fiinbas  12687  baspartn  12688  lmtopcnp  12890  rescncf  13208  limcresi  13275