Theorem ralimdva 2611

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  ralimdv  2612  ralimdvva  2613  f1mpt  5946  isores3  5990  caofrss  6300  caoftrn  6301  tfrlemibxssdm  6560  tfr1onlembxssdm  6576  tfrcllembxssdm  6589  tfrcl  6597  infidc  7203  exmidomniim  7434  exmidontri2or  7555  caucvgsrlemoffcau  8115  caucvgsrlemoffres  8117  indstr  9928  caucvgre  11670  rexuz3  11679  resqrexlemgt0  11709  resqrexlemglsq  11711  cau3lem  11803  rexanre  11909  rexico  11910  2clim  11990  climcn1  11997  climcn2  11998  subcn2  12000  climsqz  12024  climsqz2  12025  climcvg1nlem  12038  fprodsplitdc  12286  bezoutlemaz  12703  bezoutlembz  12704  bezoutlembi  12705  pcfac  13052  pockthg  13059  infpnlem1  13061  isgrpinv  13784  dfgrp3me  13830  issubg4m  13927  mplsubgfileminv  14872  cncnp  15112  txlm  15161  metequiv2  15378  metcnpi3  15399  rescncf  15463  cncfco  15473  suplociccreex  15506  limcresi  15548  cnplimcim  15549  cnplimclemr  15551  cnlimcim  15553  limccnpcntop  15557  limccoap  15560  2sqlem6  16010  wlkvtxiedg  16357  wlkvtxiedgg  16358  upgrwlkvtxedg  16376  uspgr2wlkeq  16377  clwwlkccatlem  16412  bj-charfunbi  16598  nninffeq  16815  tridceq  16858