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  5818  isores3  5862  caofrss  6162  caoftrn  6163  tfrlemibxssdm  6385  tfr1onlembxssdm  6401  tfrcllembxssdm  6414  tfrcl  6422  infidc  7000  exmidomniim  7207  exmidontri2or  7310  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  indstr  9667  caucvgre  11146  rexuz3  11155  resqrexlemgt0  11185  resqrexlemglsq  11187  cau3lem  11279  rexanre  11385  rexico  11386  2clim  11466  climcn1  11473  climcn2  11474  subcn2  11476  climsqz  11500  climsqz2  11501  climcvg1nlem  11514  fprodsplitdc  11761  bezoutlemaz  12170  bezoutlembz  12171  bezoutlembi  12172  pcfac  12519  pockthg  12526  infpnlem1  12528  isgrpinv  13186  dfgrp3me  13232  issubg4m  13323  cncnp  14466  txlm  14515  metequiv2  14732  metcnpi3  14753  rescncf  14817  cncfco  14827  suplociccreex  14860  limcresi  14902  cnplimcim  14903  cnplimclemr  14905  cnlimcim  14907  limccnpcntop  14911  limccoap  14914  2sqlem6  15361  bj-charfunbi  15457  nninffeq  15664  tridceq  15700