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

Theorem ralrimdva 2850
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 2848 1  |-  ( ph  ->  ( ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2787
This theorem is referenced by:  ralxfrd  4636  isoselem  6247  resixpfo  7568  findcard  7816  ordtypelem2  8034  alephinit  8524  isfin2-2  8747  axpre-sup  9592  nnsub  10648  ublbneg  11248  xralrple  11498  supxrunb1  11605  expnlbnd2  12400  faclbnd4lem4  12478  hashbc  12611  cau3lem  13396  limsupbnd2  13524  limsupbnd2OLD  13525  climrlim2  13589  climshftlem  13616  subcn2  13636  isercoll  13709  climsup  13711  serf0  13725  iseralt  13729  incexclem  13872  sqrt2irr  14279  pclem  14751  prmpwdvds  14811  vdwlem10  14903  vdwlem13  14906  ramtlecl  14914  ramub  14933  ramcl  14950  iscatd  15530  clatleglb  16323  mrcmndind  16564  grpinveu  16651  issubg4  16787  gexdvds  17171  sylow2alem2  17205  obselocv  19222  scmatscm  19469  tgcn  20199  tgcnp  20200  lmconst  20208  cncls2  20220  cncls  20221  cnntr  20222  lmss  20245  cnt0  20293  isnrm2  20305  isreg2  20324  cmpsublem  20345  cmpsub  20346  tgcmp  20347  islly2  20430  kgencn2  20503  txdis  20578  txlm  20594  kqt0lem  20682  isr0  20683  regr1lem2  20686  cmphaushmeo  20746  cfinufil  20874  ufilen  20876  flimopn  20921  fbflim2  20923  fclsnei  20965  fclsbas  20967  fclsrest  20970  flimfnfcls  20974  fclscmp  20976  ufilcmp  20978  isfcf  20980  fcfnei  20981  cnpfcf  20987  tsmsres  21089  tsmsxp  21100  blbas  21376  prdsbl  21437  metss  21454  metcnp3  21486  bndth  21882  lebnumii  21890  iscfil3  22136  iscmet3lem1  22154  equivcfil  22162  equivcau  22163  ellimc3  22711  lhop1  22843  dvfsumrlim  22860  ftc1lem6  22870  fta1g  22993  dgrco  23097  plydivex  23118  fta1  23129  vieta1  23133  ulmshftlem  23209  ulmcaulem  23214  mtest  23224  cxpcn3lem  23552  cxploglim  23768  ftalem3  23864  dchrisumlem3  24192  pntibnd  24294  ostth2lem2  24335  grpoinveu  25795  isgrp2d  25808  nmcvcn  26176  blocnilem  26290  ubthlem3  26359  htthlem  26405  spansni  27045  bra11  27596  lmxrge0  28597  mrsubff1  29940  msubff1  29982  fnemeet2  30808  fnejoin2  30810  fin2so  31635  poimirlem29  31672  poimirlem30  31673  ftc1cnnc  31719  incsequz2  31781  geomcau  31791  caushft  31793  sstotbnd2  31809  isbnd2  31818  totbndbnd  31824  ismtybndlem  31841  heibor  31856  atlatle  32594  cvlcvr1  32613  ltrnid  33408  ltrneq2  33421  climinf  37255  climinfOLD  37256  ralbinrald  38010  ralxfrd2  38379  snlindsntorlem  39022
  Copyright terms: Public domain W3C validator