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  6657  iinerm  6886  xpf1o  7150  exmidontriimlem3  7585  exmidontriim  7587  resqrexlemgt0  11807  cau3lem  11902  caubnd2  11905  climshftlemg  12092  climcau  12137  climcaucn  12141  serf0  12142  modfsummodlemstep  12248  bezoutlemmain  12799  ctinf  13378  strsetsid  13442  imasaddfnlemg  13693  islss4  14827  fiinbas  15292  baspartn  15293  lmtopcnp  15493  rescncf  15824  limcresi  15909  upgrwlkedg  16824  uspgr2wlkeq  16828  umgrwlknloop  16831