MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimdva Structured version   Visualization version   Unicode version

Theorem ralrimdva 2818
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.) (Proof shortened by Wolf Lammen, 28-Dec-2019.)
Hypothesis
Ref Expression
ralrimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralrimdva  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Distinct variable groups:    ph, x    ps, x
Allowed substitution hints:    ch( x)    A( x)

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21expimpd 612 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  ->  ch ) )
32expcomd 444 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2816 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2754
This theorem is referenced by:  ralxfrd  4631  isoselem  6262  resixpfo  7591  findcard  7841  ordtypelem2  8065  alephinit  8557  isfin2-2  8780  axpre-sup  9624  nnsub  10681  ublbneg  11282  xralrple  11532  supxrunb1  11639  expnlbnd2  12441  faclbnd4lem4  12519  hashbc  12655  cau3lem  13472  limsupbnd2  13601  limsupbnd2OLD  13602  climrlim2  13666  climshftlem  13693  subcn2  13713  isercoll  13786  climsup  13788  serf0  13802  iseralt  13806  incexclem  13949  sqrt2irr  14356  pclem  14843  prmpwdvds  14903  vdwlem10  14995  vdwlem13  14998  ramtlecl  15006  ramub  15025  ramcl  15042  iscatd  15634  clatleglb  16427  mrcmndind  16668  grpinveu  16755  issubg4  16891  gexdvds  17290  sylow2alem2  17325  obselocv  19346  scmatscm  19593  tgcn  20323  tgcnp  20324  lmconst  20332  cncls2  20344  cncls  20345  cnntr  20346  lmss  20369  cnt0  20417  isnrm2  20429  isreg2  20448  cmpsublem  20469  cmpsub  20470  tgcmp  20471  islly2  20554  kgencn2  20627  txdis  20702  txlm  20718  kqt0lem  20806  isr0  20807  regr1lem2  20810  cmphaushmeo  20870  cfinufil  20998  ufilen  21000  flimopn  21045  fbflim2  21047  fclsnei  21089  fclsbas  21091  fclsrest  21094  flimfnfcls  21098  fclscmp  21100  ufilcmp  21102  isfcf  21104  fcfnei  21105  cnpfcf  21111  tsmsres  21213  tsmsxp  21224  blbas  21500  prdsbl  21561  metss  21578  metcnp3  21610  bndth  22041  lebnumii  22052  iscfil3  22298  iscmet3lem1  22316  equivcfil  22324  equivcau  22325  ellimc3  22890  lhop1  23022  dvfsumrlim  23039  ftc1lem6  23049  fta1g  23174  dgrco  23285  plydivex  23306  fta1  23317  vieta1  23321  ulmshftlem  23400  ulmcaulem  23405  mtest  23415  cxpcn3lem  23743  cxploglim  23959  ftalem3  24055  dchrisumlem3  24385  pntibnd  24487  ostth2lem2  24528  grpoinveu  26006  isgrp2d  26019  nmcvcn  26387  blocnilem  26501  ubthlem3  26570  htthlem  26626  spansni  27266  bra11  27817  lmxrge0  28809  mrsubff1  30202  msubff1  30244  fnemeet2  31073  fnejoin2  31075  fin2so  31978  poimirlem29  32015  poimirlem30  32016  ftc1cnnc  32062  incsequz2  32124  geomcau  32134  caushft  32136  sstotbnd2  32152  isbnd2  32161  totbndbnd  32167  ismtybndlem  32184  heibor  32199  atlatle  32932  cvlcvr1  32951  ltrnid  33746  ltrneq2  33759  climinf  37770  climinfOLD  37771  ralbinrald  38755  ralxfrd2  39144  snlindsntorlem  40632
  Copyright terms: Public domain W3C validator