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  4441  sess1  4480  sess2  4481  riinint  5041  dffo4  5850  dffo5  5851  isoini2  6018  rdgivallem  6645  iinerm  6874  xpf1o  7137  exmidontriimlem3  7572  exmidontriim  7574  resqrexlemgt0  11767  cau3lem  11861  caubnd2  11864  climshftlemg  12049  climcau  12094  climcaucn  12098  serf0  12099  modfsummodlemstep  12205  bezoutlemmain  12756  ctinf  13302  strsetsid  13366  imasaddfnlemg  13615  islss4  14694  fiinbas  15076  baspartn  15077  lmtopcnp  15277  rescncf  15608  limcresi  15693  upgrwlkedg  16519  uspgr2wlkeq  16523  umgrwlknloop  16526