Theorem ralimdv 2618

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

Syntax hints:   -> wi 4   e. wcel 2209   A.wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  poss  4438  sess1  4477  sess2  4478  riinint  5038  dffo4  5847  dffo5  5848  isoini2  6015  rdgivallem  6642  iinerm  6871  xpf1o  7134  exmidontriimlem3  7569  exmidontriim  7571  resqrexlemgt0  11764  cau3lem  11858  caubnd2  11861  climshftlemg  12046  climcau  12091  climcaucn  12095  serf0  12096  modfsummodlemstep  12202  bezoutlemmain  12753  ctinf  13299  strsetsid  13363  imasaddfnlemg  13612  islss4  14691  fiinbas  15073  baspartn  15074  lmtopcnp  15274  rescncf  15605  limcresi  15690  upgrwlkedg  16516  uspgr2wlkeq  16520  umgrwlknloop  16523