Theorem ralimdv 2867

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1633). (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
ralimdv	|- ( 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 ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	adantr 465	. 2 |- ( ( ph /\ x e. A ) -> ( ps -> ch ) )
3	2	ralimdva 2865	1 |- ( ph -> ( A. x e. A ps -> A. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1819   A.wral 2807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812

This theorem is referenced by:  poss  4811  sess1  4856  sess2  4857  riinint  5269  iinpreima  6018  dffo4  6048  dffo5  6049  isoini2  6236  tfindsg  6694  iiner  7401  xpf1o  7698  dffi3  7909  brwdom3  8026  xpwdomg  8029  bndrank  8276  cfub  8646  cff1  8655  cfflb  8656  cfslb2n  8665  cofsmo  8666  cfcoflem  8669  pwcfsdom  8975  fpwwe2lem13  9037  inawinalem  9084  grupr  9192  fsequb  12087  cau3lem  13198  caubnd2  13201  caubnd  13202  rlim2lt  13331  rlim3  13332  climshftlem  13408  isercolllem1  13498  climcau  13504  caucvgb  13513  serf0  13514  modfsummods  13618  cvgcmp  13641  mreriincl  15014  acsfn1c  15078  islss4  17734  riinopn  19543  fiinbas  19579  baspartn  19581  isclo2  19715  lmcls  19929  lmcnp  19931  isnrm3  19986  1stcelcls  20087  llyss  20105  nllyss  20106  ptpjpre1  20197  txlly  20262  txnlly  20263  tx1stc  20276  xkococnlem  20285  fbunfip  20495  filssufilg  20537  cnpflf2  20626  fcfnei  20661  isucn2  20907  rescncf  21526  lebnum  21589  cfilss  21834  fgcfil  21835  iscau4  21843  cmetcaulem  21852  cfilres  21860  caussi  21861  ovolunlem1  22033  ulmclm  22907  ulmcaulem  22914  ulmcau  22915  ulmss  22917  rlimcnp  23420  cxploglim  23432  lgsdchr  23748  pntlemp  23920  axcontlem4  24396  usg2wlkeq  24834  3cyclfrgrarn2  25140  nmlnoubi  25837  lnon0  25839  disjpreima  27582  resspos  27799  resstos  27800  submarchi  27882  crefss  28005  iccllyscon  28870  cvmlift2lem1  28922  ss2mcls  29103  mclsax  29104  setlikess  29449  upixp  30382  caushft  30416  sstotbnd3  30434  totbndss  30435  unichnidl  30590  ispridl2  30597  elrfirn2  30790  mzpsubst  30843  eluzrabdioph  30901  fourierdlem103  32153  fourierdlem104  32154  ralralimp  32517