Theorem ralimdv 2574

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

Syntax hints:   -> wi 4   e. wcel 2176   A.wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  poss  4346  sess1  4385  sess2  4386  riinint  4940  dffo4  5730  dffo5  5731  isoini2  5890  rdgivallem  6469  iinerm  6696  xpf1o  6943  exmidontriimlem3  7337  exmidontriim  7339  resqrexlemgt0  11364  cau3lem  11458  caubnd2  11461  climshftlemg  11646  climcau  11691  climcaucn  11695  serf0  11696  modfsummodlemstep  11801  bezoutlemmain  12352  ctinf  12834  strsetsid  12898  imasaddfnlemg  13179  islss4  14177  fiinbas  14554  baspartn  14555  lmtopcnp  14755  rescncf  15086  limcresi  15171