Theorem ralimdva 2544

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

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

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  ralimdv  2545  ralimdvva  2546  f1mpt  5774  isores3  5818  caofrss  6109  caoftrn  6110  tfrlemibxssdm  6330  tfr1onlembxssdm  6346  tfrcllembxssdm  6359  tfrcl  6367  exmidomniim  7141  exmidontri2or  7244  caucvgsrlemoffcau  7799  caucvgsrlemoffres  7801  indstr  9595  caucvgre  10992  rexuz3  11001  resqrexlemgt0  11031  resqrexlemglsq  11033  cau3lem  11125  rexanre  11231  rexico  11232  2clim  11311  climcn1  11318  climcn2  11319  subcn2  11321  climsqz  11345  climsqz2  11346  climcvg1nlem  11359  fprodsplitdc  11606  bezoutlemaz  12006  bezoutlembz  12007  bezoutlembi  12008  pcfac  12350  pockthg  12357  infpnlem1  12359  isgrpinv  12931  dfgrp3me  12975  issubg4m  13058  cncnp  13769  txlm  13818  metequiv2  14035  metcnpi3  14056  rescncf  14107  cncfco  14117  suplociccreex  14141  limcresi  14174  cnplimcim  14175  cnplimclemr  14177  cnlimcim  14179  limccnpcntop  14183  limccoap  14186  2sqlem6  14506  bj-charfunbi  14602  nninffeq  14808  tridceq  14843