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  4330  sess1  4369  sess2  4370  riinint  4924  dffo4  5707  dffo5  5708  isoini2  5863  rdgivallem  6436  iinerm  6663  xpf1o  6902  exmidontriimlem3  7285  exmidontriim  7287  resqrexlemgt0  11167  cau3lem  11261  caubnd2  11264  climshftlemg  11448  climcau  11493  climcaucn  11497  serf0  11498  modfsummodlemstep  11603  bezoutlemmain  12138  ctinf  12590  strsetsid  12654  imasaddfnlemg  12900  islss4  13881  fiinbas  14228  baspartn  14229  lmtopcnp  14429  rescncf  14760  limcresi  14845