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  5977  isores3  6021  caofrss  6334  caoftrn  6335  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  tfrcl  6635  infidc  7248  exmidomniim  7481  exmidontri2or  7602  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  indstr  10002  caucvgre  11761  rexuz3  11770  resqrexlemgt0  11800  resqrexlemglsq  11802  cau3lem  11895  rexanre  12001  rexico  12002  2clim  12083  climcn1  12090  climcn2  12091  subcn2  12093  climsqz  12117  climsqz2  12118  climcvg1nlem  12131  fprodsplitdc  12379  bezoutlemaz  12796  bezoutlembz  12797  bezoutlembi  12798  sqrtrirr  13005  pcfac  13149  pockthg  13156  infpnlem1  13158  isgrpinv  13908  dfgrp3me  13954  issubg4m  14045  mplsubgfileminv  15140  cncnp  15380  txlm  15429  metequiv2  15646  metcnpi3  15667  rescncf  15731  cncfco  15741  suplociccreex  15774  limcresi  15816  cnplimcim  15817  cnplimclemr  15819  cnlimcim  15821  limccnpcntop  15825  limccoap  15828  2sqlem6  16337  wlkvtxiedg  16684  wlkvtxiedgg  16685  upgrwlkvtxedg  16703  uspgr2wlkeq  16704  clwwlkccatlem  16739  bj-charfunbi  16935  nninffeq  17161  tridceq  17204