Theorem ralimdv 2598

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

Syntax hints:   -> wi 4   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  poss  4389  sess1  4428  sess2  4429  riinint  4985  dffo4  5785  dffo5  5786  isoini2  5949  rdgivallem  6533  iinerm  6762  xpf1o  7013  exmidontriimlem3  7416  exmidontriim  7418  resqrexlemgt0  11547  cau3lem  11641  caubnd2  11644  climshftlemg  11829  climcau  11874  climcaucn  11878  serf0  11879  modfsummodlemstep  11984  bezoutlemmain  12535  ctinf  13017  strsetsid  13081  imasaddfnlemg  13363  islss4  14362  fiinbas  14739  baspartn  14740  lmtopcnp  14940  rescncf  15271  limcresi  15356  upgrwlkedg  16107  uspgr2wlkeq  16111  umgrwlknloop  16114