Theorem ralimdv 2618

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  poss  4445  sess1  4484  sess2  4485  riinint  5045  dffo4  5859  dffo5  5860  isoini2  6028  rdgivallem  6656  iinerm  6885  xpf1o  7148  exmidontriimlem3  7585  exmidontriim  7587  resqrexlemgt0  11808  cau3lem  11903  caubnd2  11906  climshftlemg  12093  climcau  12138  climcaucn  12142  serf0  12143  modfsummodlemstep  12249  bezoutlemmain  12800  ctinf  13379  strsetsid  13443  imasaddfnlemg  13694  islss4  14828  fiinbas  15275  baspartn  15276  lmtopcnp  15476  rescncf  15807  limcresi  15892  upgrwlkedg  16807  uspgr2wlkeq  16811  umgrwlknloop  16814