Theorem ralimdva 2524

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

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

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 1427  ax-gen 1429  ax-4 1490  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440

This theorem is referenced by:  ralimdv  2525  ralimdvva  2526  f1mpt  5721  isores3  5765  caofrss  6056  caoftrn  6057  tfrlemibxssdm  6274  tfr1onlembxssdm  6290  tfrcllembxssdm  6303  tfrcl  6311  exmidomniim  7084  exmidontri2or  7178  caucvgsrlemoffcau  7718  caucvgsrlemoffres  7720  indstr  9504  caucvgre  10881  rexuz3  10890  resqrexlemgt0  10920  resqrexlemglsq  10922  cau3lem  11014  rexanre  11120  rexico  11121  2clim  11198  climcn1  11205  climcn2  11206  subcn2  11208  climsqz  11232  climsqz2  11233  climcvg1nlem  11246  fprodsplitdc  11493  bezoutlemaz  11886  bezoutlembz  11887  bezoutlembi  11888  cncnp  12630  txlm  12679  metequiv2  12896  metcnpi3  12917  rescncf  12968  cncfco  12978  suplociccreex  13002  limcresi  13035  cnplimcim  13036  cnplimclemr  13038  cnlimcim  13040  limccnpcntop  13044  limccoap  13047  bj-charfunbi  13386  nninffeq  13592  tridceq  13627