Theorem ralimdva 2564

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  ralimdv  2565  ralimdvva  2566  f1mpt  5819  isores3  5863  caofrss  6163  caoftrn  6164  tfrlemibxssdm  6386  tfr1onlembxssdm  6402  tfrcllembxssdm  6415  tfrcl  6423  infidc  7001  exmidomniim  7208  exmidontri2or  7312  caucvgsrlemoffcau  7867  caucvgsrlemoffres  7869  indstr  9669  caucvgre  11148  rexuz3  11157  resqrexlemgt0  11187  resqrexlemglsq  11189  cau3lem  11281  rexanre  11387  rexico  11388  2clim  11468  climcn1  11475  climcn2  11476  subcn2  11478  climsqz  11502  climsqz2  11503  climcvg1nlem  11516  fprodsplitdc  11763  bezoutlemaz  12180  bezoutlembz  12181  bezoutlembi  12182  pcfac  12529  pockthg  12536  infpnlem1  12538  isgrpinv  13196  dfgrp3me  13242  issubg4m  13333  cncnp  14476  txlm  14525  metequiv2  14742  metcnpi3  14763  rescncf  14827  cncfco  14837  suplociccreex  14870  limcresi  14912  cnplimcim  14913  cnplimclemr  14915  cnlimcim  14917  limccnpcntop  14921  limccoap  14924  2sqlem6  15371  bj-charfunbi  15467  nninffeq  15674  tridceq  15710