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

Theorem ralrimdva 2882
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 603 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  ->  ch ) )
32expcomd 438 . 2  |-  ( ph  ->  ( ps  ->  (
x  e.  A  ->  ch ) ) )
43ralrimdv 2880 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819
This theorem is referenced by:  ralxfrd  4661  isoselem  6223  resixpfo  7504  findcard  7755  ordtypelem2  7940  alephinit  8472  isfin2-2  8695  axpre-sup  9542  nnsub  10570  ublbneg  11162  xralrple  11400  supxrunb1  11507  expnlbnd2  12261  faclbnd4lem4  12338  hashbc  12464  cau3lem  13146  limsupbnd2  13265  climrlim2  13329  climshftlem  13356  subcn2  13376  isercoll  13449  climsup  13451  serf0  13462  iseralt  13466  incexclem  13607  sqrt2irr  13839  pclem  14217  prmpwdvds  14277  vdwlem10  14363  vdwlem13  14366  ramtlecl  14373  ramub  14386  ramcl  14402  iscatd  14924  clatleglb  15609  mrcmndind  15807  grpinveu  15885  issubg4  16015  gexdvds  16400  sylow2alem2  16434  obselocv  18526  tgcn  19519  tgcnp  19520  lmconst  19528  cncls2  19540  cncls  19541  cnntr  19542  lmss  19565  cnt0  19613  isnrm2  19625  isreg2  19644  cmpsublem  19665  cmpsub  19666  tgcmp  19667  islly2  19751  kgencn2  19793  txdis  19868  txlm  19884  kqt0lem  19972  isr0  19973  regr1lem2  19976  cmphaushmeo  20036  cfinufil  20164  ufilen  20166  flimopn  20211  fbflim2  20213  fclsnei  20255  fclsbas  20257  fclsrest  20260  flimfnfcls  20264  fclscmp  20266  ufilcmp  20268  isfcf  20270  fcfnei  20271  cnpfcf  20277  tsmsresOLD  20380  tsmsres  20381  tsmsxp  20392  blbas  20668  prdsbl  20729  metss  20746  metcnp3  20778  bndth  21193  lebnumii  21201  iscfil3  21447  iscmet3lem1  21465  equivcfil  21473  equivcau  21474  ellimc3  22018  lhop1  22150  dvfsumrlim  22167  ftc1lem6  22177  fta1g  22303  dgrco  22406  plydivex  22427  fta1  22438  vieta1  22442  ulmshftlem  22518  ulmcaulem  22523  mtest  22533  cxpcn3lem  22849  cxploglim  23035  ftalem3  23076  dchrisumlem3  23404  pntibnd  23506  ostth2lem2  23547  grpoinveu  24900  isgrp2d  24913  nmcvcn  25281  blocnilem  25395  ubthlem3  25464  htthlem  25510  spansni  26151  bra11  26703  lmxrge0  27570  fin2so  29617  ftc1cnnc  29666  fnemeet2  29788  fnejoin2  29790  incsequz2  29845  geomcau  29855  caushft  29857  sstotbnd2  29873  isbnd2  29882  totbndbnd  29888  ismtybndlem  29905  heibor  29920  climinf  31148  ralbinrald  31671  ralxfrd2  31770  atlatle  34117  cvlcvr1  34136  ltrnid  34931  ltrneq2  34944
  Copyright terms: Public domain W3C validator