Theorem ralimdva 2561

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  ralimdv  2562  ralimdvva  2563  f1mpt  5815  isores3  5859  caofrss  6159  caoftrn  6160  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  tfrcl  6419  infidc  6995  exmidomniim  7202  exmidontri2or  7305  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  indstr  9661  caucvgre  11128  rexuz3  11137  resqrexlemgt0  11167  resqrexlemglsq  11169  cau3lem  11261  rexanre  11367  rexico  11368  2clim  11447  climcn1  11454  climcn2  11455  subcn2  11457  climsqz  11481  climsqz2  11482  climcvg1nlem  11495  fprodsplitdc  11742  bezoutlemaz  12143  bezoutlembz  12144  bezoutlembi  12145  pcfac  12491  pockthg  12498  infpnlem1  12500  isgrpinv  13129  dfgrp3me  13175  issubg4m  13266  cncnp  14409  txlm  14458  metequiv2  14675  metcnpi3  14696  rescncf  14760  cncfco  14770  suplociccreex  14803  limcresi  14845  cnplimcim  14846  cnplimclemr  14848  cnlimcim  14850  limccnpcntop  14854  limccoap  14857  2sqlem6  15277  bj-charfunbi  15373  nninffeq  15580  tridceq  15616