Theorem ralimdva 2600

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 2599	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

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

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 2516

This theorem is referenced by:  ralimdv  2601  ralimdvva  2602  f1mpt  5922  isores3  5966  caofrss  6276  caoftrn  6277  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  tfrcl  6573  infidc  7176  exmidomniim  7400  exmidontri2or  7521  caucvgsrlemoffcau  8078  caucvgsrlemoffres  8080  indstr  9888  caucvgre  11621  rexuz3  11630  resqrexlemgt0  11660  resqrexlemglsq  11662  cau3lem  11754  rexanre  11860  rexico  11861  2clim  11941  climcn1  11948  climcn2  11949  subcn2  11951  climsqz  11975  climsqz2  11976  climcvg1nlem  11989  fprodsplitdc  12237  bezoutlemaz  12654  bezoutlembz  12655  bezoutlembi  12656  pcfac  13003  pockthg  13010  infpnlem1  13012  isgrpinv  13717  dfgrp3me  13763  issubg4m  13860  mplsubgfileminv  14801  cncnp  15041  txlm  15090  metequiv2  15307  metcnpi3  15328  rescncf  15392  cncfco  15402  suplociccreex  15435  limcresi  15477  cnplimcim  15478  cnplimclemr  15480  cnlimcim  15482  limccnpcntop  15486  limccoap  15489  2sqlem6  15939  wlkvtxiedg  16286  wlkvtxiedgg  16287  upgrwlkvtxedg  16305  uspgr2wlkeq  16306  clwwlkccatlem  16341  bj-charfunbi  16527  nninffeq  16746  tridceq  16789