Theorem ralimdva 2573

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

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

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489

This theorem is referenced by:  ralimdv  2574  ralimdvva  2575  f1mpt  5842  isores3  5886  caofrss  6192  caoftrn  6193  tfrlemibxssdm  6415  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  tfrcl  6452  infidc  7038  exmidomniim  7245  exmidontri2or  7357  caucvgsrlemoffcau  7913  caucvgsrlemoffres  7915  indstr  9716  caucvgre  11325  rexuz3  11334  resqrexlemgt0  11364  resqrexlemglsq  11366  cau3lem  11458  rexanre  11564  rexico  11565  2clim  11645  climcn1  11652  climcn2  11653  subcn2  11655  climsqz  11679  climsqz2  11680  climcvg1nlem  11693  fprodsplitdc  11940  bezoutlemaz  12357  bezoutlembz  12358  bezoutlembi  12359  pcfac  12706  pockthg  12713  infpnlem1  12715  isgrpinv  13419  dfgrp3me  13465  issubg4m  13562  mplsubgfileminv  14495  cncnp  14735  txlm  14784  metequiv2  15001  metcnpi3  15022  rescncf  15086  cncfco  15096  suplociccreex  15129  limcresi  15171  cnplimcim  15172  cnplimclemr  15174  cnlimcim  15176  limccnpcntop  15180  limccoap  15183  2sqlem6  15630  bj-charfunbi  15784  nninffeq  15994  tridceq  16032