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  5783  dffo5  5784  isoini2  5943  rdgivallem  6527  iinerm  6754  xpf1o  7005  exmidontriimlem3  7405  exmidontriim  7407  resqrexlemgt0  11531  cau3lem  11625  caubnd2  11628  climshftlemg  11813  climcau  11858  climcaucn  11862  serf0  11863  modfsummodlemstep  11968  bezoutlemmain  12519  ctinf  13001  strsetsid  13065  imasaddfnlemg  13347  islss4  14346  fiinbas  14723  baspartn  14724  lmtopcnp  14924  rescncf  15255  limcresi  15340  upgrwlkedg  16072  uspgr2wlkeq  16076  umgrwlknloop  16079