Theorem ralimdv 2612

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

Syntax hints:   -> wi 4   e. wcel 2205   A.wral 2522

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  poss  4424  sess1  4463  sess2  4464  riinint  5023  dffo4  5830  dffo5  5831  isoini2  5998  rdgivallem  6625  iinerm  6854  xpf1o  7110  exmidontriimlem3  7543  exmidontriim  7545  resqrexlemgt0  11730  cau3lem  11824  caubnd2  11827  climshftlemg  12012  climcau  12057  climcaucn  12061  serf0  12062  modfsummodlemstep  12168  bezoutlemmain  12719  ctinf  13265  strsetsid  13329  imasaddfnlemg  13578  islss4  14656  fiinbas  15040  baspartn  15041  lmtopcnp  15241  rescncf  15572  limcresi  15657  upgrwlkedg  16482  uspgr2wlkeq  16486  umgrwlknloop  16489