Theorem ralimdv 2601

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

Syntax hints:   -> wi 4   e. wcel 2202   A.wral 2511

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  poss  4401  sess1  4440  sess2  4441  riinint  4999  dffo4  5803  dffo5  5804  isoini2  5970  rdgivallem  6590  iinerm  6819  xpf1o  7073  exmidontriimlem3  7498  exmidontriim  7500  resqrexlemgt0  11660  cau3lem  11754  caubnd2  11757  climshftlemg  11942  climcau  11987  climcaucn  11991  serf0  11992  modfsummodlemstep  12098  bezoutlemmain  12649  ctinf  13131  strsetsid  13195  imasaddfnlemg  13477  islss4  14478  fiinbas  14860  baspartn  14861  lmtopcnp  15061  rescncf  15392  limcresi  15477  upgrwlkedg  16302  uspgr2wlkeq  16306  umgrwlknloop  16309