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  7580  exmidontriim  7582  resqrexlemgt0  11802  cau3lem  11897  caubnd2  11900  climshftlemg  12087  climcau  12132  climcaucn  12136  serf0  12137  modfsummodlemstep  12243  bezoutlemmain  12794  ctinf  13373  strsetsid  13437  imasaddfnlemg  13688  islss4  14803  fiinbas  15241  baspartn  15242  lmtopcnp  15442  rescncf  15773  limcresi  15858  upgrwlkedg  16768  uspgr2wlkeq  16772  umgrwlknloop  16775