Theorem ralimdva 2597

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralimdv  2598  ralimdvva  2599  f1mpt  5901  isores3  5945  caofrss  6256  caoftrn  6257  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  tfrcl  6516  infidc  7112  exmidomniim  7319  exmidontri2or  7439  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  indstr  9800  caucvgre  11508  rexuz3  11517  resqrexlemgt0  11547  resqrexlemglsq  11549  cau3lem  11641  rexanre  11747  rexico  11748  2clim  11828  climcn1  11835  climcn2  11836  subcn2  11838  climsqz  11862  climsqz2  11863  climcvg1nlem  11876  fprodsplitdc  12123  bezoutlemaz  12540  bezoutlembz  12541  bezoutlembi  12542  pcfac  12889  pockthg  12896  infpnlem1  12898  isgrpinv  13603  dfgrp3me  13649  issubg4m  13746  mplsubgfileminv  14680  cncnp  14920  txlm  14969  metequiv2  15186  metcnpi3  15207  rescncf  15271  cncfco  15281  suplociccreex  15314  limcresi  15356  cnplimcim  15357  cnplimclemr  15359  cnlimcim  15361  limccnpcntop  15365  limccoap  15368  2sqlem6  15815  wlkvtxiedg  16091  wlkvtxiedgg  16092  upgrwlkvtxedg  16110  uspgr2wlkeq  16111  clwwlkccatlem  16143  bj-charfunbi  16257  nninffeq  16474  tridceq  16512