Theorem ralimdv 2522

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

Syntax hints:   -> wi 4   e. wcel 2125   A.wral 2432

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 1424  ax-gen 1426  ax-4 1487  ax-17 1503

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2437

This theorem is referenced by:  poss  4253  sess1  4292  sess2  4293  riinint  4840  dffo4  5608  dffo5  5609  isoini2  5760  rdgivallem  6318  iinerm  6541  xpf1o  6778  exmidontriimlem3  7137  exmidontriim  7139  resqrexlemgt0  10897  cau3lem  10991  caubnd2  10994  climshftlemg  11176  climcau  11221  climcaucn  11225  serf0  11226  modfsummodlemstep  11331  bezoutlemmain  11854  ctinf  12118  strsetsid  12170  fiinbas  12394  baspartn  12395  lmtopcnp  12597  rescncf  12915  limcresi  12982