Theorem ralimdv 2388

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 261	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2387	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1393   A.wral 2306

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311

This theorem is referenced by:  poss  4035  sess1  4074  sess2  4075  riinint  4593  dffo4  5315  dffo5  5316  isoini2  5458  rdgivallem  5968  iinerm  6178  resqrexlemgt0  9618  cau3lem  9710  caubnd2  9713  climshftlemg  9823  climcau  9866  climcaucn  9870  serif0  9871