Theorem ralimdva 2617

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralimdv  2618  ralimdvva  2619  f1mpt  5980  isores3  6024  caofrss  6338  caoftrn  6339  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  tfrcl  6640  infidc  7254  exmidomniim  7487  exmidontri2or  7608  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  indstr  10008  caucvgre  11768  rexuz3  11777  resqrexlemgt0  11807  resqrexlemglsq  11809  cau3lem  11902  rexanre  12008  rexico  12009  fiidxsupcl  12017  2clim  12091  climcn1  12098  climcn2  12099  subcn2  12101  climsqz  12125  climsqz2  12126  climcvg1nlem  12139  fprodsplitdc  12387  bezoutlemaz  12804  bezoutlembz  12805  bezoutlembi  12806  sqrtrirr  13013  pcfac  13157  pockthg  13164  infpnlem1  13166  isgrpinv  13917  dfgrp3me  13963  issubg4m  14054  psrbagmaxlem1  15178  mplsubgfileminv  15233  cncnp  15473  txlm  15522  metequiv2  15739  metcnpi3  15760  rescncf  15824  cncfco  15834  suplociccreex  15867  limcresi  15909  cnplimcim  15910  cnplimclemr  15912  cnlimcim  15914  limccnpcntop  15918  limccoap  15921  2sqlem6  16461  wlkvtxiedg  16808  wlkvtxiedgg  16809  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  clwwlkccatlem  16863  bj-charfunbi  17059  nninffeq  17286  tridceq  17330