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  13815  txlm  13864  metequiv2  14081  metcnpi3  14102  rescncf  14153  cncfco  14163  suplociccreex  14187  limcresi  14220  cnplimcim  14221  cnplimclemr  14223  cnlimcim  14225  limccnpcntop  14229  limccoap  14232  2sqlem6  14552  bj-charfunbi  14648  nninffeq  14854  tridceq  14889