Theorem ralimdva 2597

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)

Hypothesis

Ref	Expression
ralimdva.1	|- ( ( ph /\ x e. A ) -> ( ps -> ch ) )

Assertion

Ref	Expression
ralimdva	|- ( 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 ralimdva

Step	Hyp	Ref	Expression
1		nfv 1574	. 2 |- F/ x ph
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	ralimdaa 2596	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralimdv  2598  ralimdvva  2599  f1mpt  5895  isores3  5939  caofrss  6250  caoftrn  6251  tfrlemibxssdm  6473  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  tfrcl  6510  infidc  7101  exmidomniim  7308  exmidontri2or  7428  caucvgsrlemoffcau  7985  caucvgsrlemoffres  7987  indstr  9788  caucvgre  11492  rexuz3  11501  resqrexlemgt0  11531  resqrexlemglsq  11533  cau3lem  11625  rexanre  11731  rexico  11732  2clim  11812  climcn1  11819  climcn2  11820  subcn2  11822  climsqz  11846  climsqz2  11847  climcvg1nlem  11860  fprodsplitdc  12107  bezoutlemaz  12524  bezoutlembz  12525  bezoutlembi  12526  pcfac  12873  pockthg  12880  infpnlem1  12882  isgrpinv  13587  dfgrp3me  13633  issubg4m  13730  mplsubgfileminv  14664  cncnp  14904  txlm  14953  metequiv2  15170  metcnpi3  15191  rescncf  15255  cncfco  15265  suplociccreex  15298  limcresi  15340  cnplimcim  15341  cnplimclemr  15343  cnlimcim  15345  limccnpcntop  15349  limccoap  15352  2sqlem6  15799  wlkvtxiedg  16056  wlkvtxiedgg  16057  upgrwlkvtxedg  16075  uspgr2wlkeq  16076  bj-charfunbi  16174  nninffeq  16386  tridceq  16424