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

Theorem ralrimdva 2840
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 606 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  ->  ch ) )
32expcomd 439 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2838 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   A.wral 2771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2776
This theorem is referenced by:  ralxfrd  4635  isoselem  6247  resixpfo  7571  findcard  7819  ordtypelem2  8043  alephinit  8533  isfin2-2  8756  axpre-sup  9600  nnsub  10655  ublbneg  11255  xralrple  11505  supxrunb1  11612  expnlbnd2  12409  faclbnd4lem4  12487  hashbc  12620  cau3lem  13417  limsupbnd2  13545  limsupbnd2OLD  13546  climrlim2  13610  climshftlem  13637  subcn2  13657  isercoll  13730  climsup  13732  serf0  13746  iseralt  13750  incexclem  13893  sqrt2irr  14300  pclem  14787  prmpwdvds  14847  vdwlem10  14939  vdwlem13  14942  ramtlecl  14950  ramub  14969  ramcl  14986  iscatd  15578  clatleglb  16371  mrcmndind  16612  grpinveu  16699  issubg4  16835  gexdvds  17234  sylow2alem2  17269  obselocv  19289  scmatscm  19536  tgcn  20266  tgcnp  20267  lmconst  20275  cncls2  20287  cncls  20288  cnntr  20289  lmss  20312  cnt0  20360  isnrm2  20372  isreg2  20391  cmpsublem  20412  cmpsub  20413  tgcmp  20414  islly2  20497  kgencn2  20570  txdis  20645  txlm  20661  kqt0lem  20749  isr0  20750  regr1lem2  20753  cmphaushmeo  20813  cfinufil  20941  ufilen  20943  flimopn  20988  fbflim2  20990  fclsnei  21032  fclsbas  21034  fclsrest  21037  flimfnfcls  21041  fclscmp  21043  ufilcmp  21045  isfcf  21047  fcfnei  21048  cnpfcf  21054  tsmsres  21156  tsmsxp  21167  blbas  21443  prdsbl  21504  metss  21521  metcnp3  21553  bndth  21984  lebnumii  21995  iscfil3  22241  iscmet3lem1  22259  equivcfil  22267  equivcau  22268  ellimc3  22832  lhop1  22964  dvfsumrlim  22981  ftc1lem6  22991  fta1g  23116  dgrco  23227  plydivex  23248  fta1  23259  vieta1  23263  ulmshftlem  23342  ulmcaulem  23347  mtest  23357  cxpcn3lem  23685  cxploglim  23901  ftalem3  23997  dchrisumlem3  24327  pntibnd  24429  ostth2lem2  24470  grpoinveu  25948  isgrp2d  25961  nmcvcn  26329  blocnilem  26443  ubthlem3  26512  htthlem  26568  spansni  27208  bra11  27759  lmxrge0  28766  mrsubff1  30160  msubff1  30202  fnemeet2  31028  fnejoin2  31030  fin2so  31896  poimirlem29  31933  poimirlem30  31934  ftc1cnnc  31980  incsequz2  32042  geomcau  32052  caushft  32054  sstotbnd2  32070  isbnd2  32079  totbndbnd  32085  ismtybndlem  32102  heibor  32117  atlatle  32855  cvlcvr1  32874  ltrnid  33669  ltrneq2  33682  climinf  37624  climinfOLD  37625  ralbinrald  38491  ralxfrd2  38872  snlindsntorlem  39885
  Copyright terms: Public domain W3C validator