Theorem ralimdv 2545

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

Syntax hints:   -> wi 4   e. wcel 2148   A.wral 2455

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  poss  4300  sess1  4339  sess2  4340  riinint  4890  dffo4  5666  dffo5  5667  isoini2  5822  rdgivallem  6384  iinerm  6609  xpf1o  6846  exmidontriimlem3  7224  exmidontriim  7226  resqrexlemgt0  11031  cau3lem  11125  caubnd2  11128  climshftlemg  11312  climcau  11357  climcaucn  11361  serf0  11362  modfsummodlemstep  11467  bezoutlemmain  12001  ctinf  12433  strsetsid  12497  imasaddfnlemg  12740  islss4  13474  fiinbas  13634  baspartn  13635  lmtopcnp  13835  rescncf  14153  limcresi  14220