Theorem ralimdva 2599

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 1576	. 2 |- F/ x ph
2		ralimdva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	1, 2	ralimdaa 2598	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralimdv  2600  ralimdvva  2601  f1mpt  5912  isores3  5956  caofrss  6267  caoftrn  6268  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  tfrcl  6530  infidc  7133  exmidomniim  7340  exmidontri2or  7461  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  indstr  9827  caucvgre  11559  rexuz3  11568  resqrexlemgt0  11598  resqrexlemglsq  11600  cau3lem  11692  rexanre  11798  rexico  11799  2clim  11879  climcn1  11886  climcn2  11887  subcn2  11889  climsqz  11913  climsqz2  11914  climcvg1nlem  11927  fprodsplitdc  12175  bezoutlemaz  12592  bezoutlembz  12593  bezoutlembi  12594  pcfac  12941  pockthg  12948  infpnlem1  12950  isgrpinv  13655  dfgrp3me  13701  issubg4m  13798  mplsubgfileminv  14733  cncnp  14973  txlm  15022  metequiv2  15239  metcnpi3  15260  rescncf  15324  cncfco  15334  suplociccreex  15367  limcresi  15409  cnplimcim  15410  cnplimclemr  15412  cnlimcim  15414  limccnpcntop  15418  limccoap  15421  2sqlem6  15868  wlkvtxiedg  16215  wlkvtxiedgg  16216  upgrwlkvtxedg  16234  uspgr2wlkeq  16235  clwwlkccatlem  16270  bj-charfunbi  16457  nninffeq  16673  tridceq  16712