Theorem ralimdv 2558

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

Syntax hints:   -> wi 4   e. wcel 2160   A.wral 2468

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 2473

This theorem is referenced by:  poss  4323  sess1  4362  sess2  4363  riinint  4913  dffo4  5692  dffo5  5693  isoini2  5848  rdgivallem  6414  iinerm  6641  xpf1o  6880  exmidontriimlem3  7262  exmidontriim  7264  resqrexlemgt0  11076  cau3lem  11170  caubnd2  11173  climshftlemg  11357  climcau  11402  climcaucn  11406  serf0  11407  modfsummodlemstep  11512  bezoutlemmain  12046  ctinf  12498  strsetsid  12562  imasaddfnlemg  12808  islss4  13741  fiinbas  14070  baspartn  14071  lmtopcnp  14271  rescncf  14589  limcresi  14673