Theorem ralimdva 2533

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

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  ralimdv  2534  ralimdvva  2535  f1mpt  5739  isores3  5783  caofrss  6074  caoftrn  6075  tfrlemibxssdm  6295  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  tfrcl  6332  exmidomniim  7105  exmidontri2or  7199  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  indstr  9531  caucvgre  10923  rexuz3  10932  resqrexlemgt0  10962  resqrexlemglsq  10964  cau3lem  11056  rexanre  11162  rexico  11163  2clim  11242  climcn1  11249  climcn2  11250  subcn2  11252  climsqz  11276  climsqz2  11277  climcvg1nlem  11290  fprodsplitdc  11537  bezoutlemaz  11936  bezoutlembz  11937  bezoutlembi  11938  pcfac  12280  pockthg  12287  infpnlem1  12289  cncnp  12870  txlm  12919  metequiv2  13136  metcnpi3  13157  rescncf  13208  cncfco  13218  suplociccreex  13242  limcresi  13275  cnplimcim  13276  cnplimclemr  13278  cnlimcim  13280  limccnpcntop  13284  limccoap  13287  2sqlem6  13596  bj-charfunbi  13693  nninffeq  13900  tridceq  13935