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 ) )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  poss  4443  sess1  4482  sess2  4483  riinint  5043  dffo4  5856  dffo5  5857  isoini2  6025  rdgivallem  6652  iinerm  6881  xpf1o  7144  exmidontriimlem3  7579  exmidontriim  7581  resqrexlemgt0  11786  cau3lem  11880  caubnd2  11883  climshftlemg  12068  climcau  12113  climcaucn  12117  serf0  12118  modfsummodlemstep  12224  bezoutlemmain  12775  ctinf  13321  strsetsid  13385  imasaddfnlemg  13635  islss4  14719  fiinbas  15150  baspartn  15151  lmtopcnp  15351  rescncf  15682  limcresi  15767  upgrwlkedg  16602  uspgr2wlkeq  16606  umgrwlknloop  16609