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  5821  isores3  5865  caofrss  6171  caoftrn  6172  tfrlemibxssdm  6394  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  tfrcl  6431  infidc  7009  exmidomniim  7216  exmidontri2or  7326  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  indstr  9684  caucvgre  11163  rexuz3  11172  resqrexlemgt0  11202  resqrexlemglsq  11204  cau3lem  11296  rexanre  11402  rexico  11403  2clim  11483  climcn1  11490  climcn2  11491  subcn2  11493  climsqz  11517  climsqz2  11518  climcvg1nlem  11531  fprodsplitdc  11778  bezoutlemaz  12195  bezoutlembz  12196  bezoutlembi  12197  pcfac  12544  pockthg  12551  infpnlem1  12553  isgrpinv  13256  dfgrp3me  13302  issubg4m  13399  cncnp  14550  txlm  14599  metequiv2  14816  metcnpi3  14837  rescncf  14901  cncfco  14911  suplociccreex  14944  limcresi  14986  cnplimcim  14987  cnplimclemr  14989  cnlimcim  14991  limccnpcntop  14995  limccoap  14998  2sqlem6  15445  bj-charfunbi  15541  nninffeq  15751  tridceq  15787