Theorem ralimdva 2502

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1481   A.wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422

This theorem is referenced by:  ralimdv  2503  ralimdvva  2504  f1mpt  5680  isores3  5724  caofrss  6014  caoftrn  6015  tfrlemibxssdm  6232  tfr1onlembxssdm  6248  tfrcllembxssdm  6261  tfrcl  6269  exmidomniim  7021  caucvgsrlemoffcau  7630  caucvgsrlemoffres  7632  indstr  9415  caucvgre  10785  rexuz3  10794  resqrexlemgt0  10824  resqrexlemglsq  10826  cau3lem  10918  rexanre  11024  rexico  11025  2clim  11102  climcn1  11109  climcn2  11110  subcn2  11112  climsqz  11136  climsqz2  11137  climcvg1nlem  11150  bezoutlemaz  11727  bezoutlembz  11728  bezoutlembi  11729  cncnp  12438  txlm  12487  metequiv2  12704  metcnpi3  12725  rescncf  12776  cncfco  12786  suplociccreex  12810  limcresi  12843  cnplimcim  12844  cnplimclemr  12846  cnlimcim  12848  limccnpcntop  12852  limccoap  12855  nninffeq  13391