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  9993  caucvgre  11747  rexuz3  11756  resqrexlemgt0  11786  resqrexlemglsq  11788  cau3lem  11880  rexanre  11986  rexico  11987  2clim  12067  climcn1  12074  climcn2  12075  subcn2  12077  climsqz  12101  climsqz2  12102  climcvg1nlem  12115  fprodsplitdc  12363  bezoutlemaz  12780  bezoutlembz  12781  bezoutlembi  12782  pcfac  13129  pockthg  13136  infpnlem1  13138  isgrpinv  13859  dfgrp3me  13905  issubg4m  13996  mplsubgfileminv  15091  cncnp  15331  txlm  15380  metequiv2  15597  metcnpi3  15618  rescncf  15682  cncfco  15692  suplociccreex  15725  limcresi  15767  cnplimcim  15768  cnplimclemr  15770  cnlimcim  15772  limccnpcntop  15776  limccoap  15779  2sqlem6  16239  wlkvtxiedg  16586  wlkvtxiedgg  16587  upgrwlkvtxedg  16605  uspgr2wlkeq  16606  clwwlkccatlem  16641  bj-charfunbi  16837  nninffeq  17063  tridceq  17106