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  5775  isores3  5819  caofrss  6110  caoftrn  6111  tfrlemibxssdm  6331  tfr1onlembxssdm  6347  tfrcllembxssdm  6360  tfrcl  6368  exmidomniim  7142  exmidontri2or  7245  caucvgsrlemoffcau  7800  caucvgsrlemoffres  7802  indstr  9596  caucvgre  10993  rexuz3  11002  resqrexlemgt0  11032  resqrexlemglsq  11034  cau3lem  11126  rexanre  11232  rexico  11233  2clim  11312  climcn1  11319  climcn2  11320  subcn2  11322  climsqz  11346  climsqz2  11347  climcvg1nlem  11360  fprodsplitdc  11607  bezoutlemaz  12007  bezoutlembz  12008  bezoutlembi  12009  pcfac  12351  pockthg  12358  infpnlem1  12360  isgrpinv  12932  dfgrp3me  12976  issubg4m  13059  cncnp  13870  txlm  13919  metequiv2  14136  metcnpi3  14157  rescncf  14208  cncfco  14218  suplociccreex  14242  limcresi  14275  cnplimcim  14276  cnplimclemr  14278  cnlimcim  14280  limccnpcntop  14284  limccoap  14287  2sqlem6  14607  bj-charfunbi  14703  nninffeq  14910  tridceq  14945