Theorem ralimdv 2562

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

Syntax hints:   -> wi 4   e. wcel 2164   A.wral 2472

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  poss  4329  sess1  4368  sess2  4369  riinint  4923  dffo4  5706  dffo5  5707  isoini2  5862  rdgivallem  6434  iinerm  6661  xpf1o  6900  exmidontriimlem3  7283  exmidontriim  7285  resqrexlemgt0  11164  cau3lem  11258  caubnd2  11261  climshftlemg  11445  climcau  11490  climcaucn  11494  serf0  11495  modfsummodlemstep  11600  bezoutlemmain  12135  ctinf  12587  strsetsid  12651  imasaddfnlemg  12897  islss4  13878  fiinbas  14217  baspartn  14218  lmtopcnp  14418  rescncf  14736  limcresi  14820