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

Theorem ralrimdva 3157
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 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralrimdva (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜓,𝑥
Allowed substitution hints:   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21expimpd 443 . . 3 (𝜑 → ((𝑥𝐴𝜓) → 𝜒))
32expcomd 404 . 2 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
43ralrimdv 3156 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ral 3101
This theorem is referenced by:  ralxfrd  5077  ralxfrd2  5081  isoselem  6815  resixpfo  8183  findcard  8438  ordtypelem2  8663  alephinit  9201  isfin2-2  9426  axpre-sup  10275  nnsub  11345  ublbneg  11992  xralrple  12254  supxrunb1  12367  expnlbnd2  13218  faclbnd4lem4  13303  hashbc  13454  cau3lem  14317  limsupbnd2  14437  climrlim2  14501  climshftlem  14528  subcn2  14548  isercoll  14621  climsup  14623  serf0  14634  iseralt  14638  incexclem  14790  sqrt2irr  15199  pclem  15760  prmpwdvds  15825  vdwlem10  15911  vdwlem13  15914  ramtlecl  15921  ramub  15934  ramcl  15950  iscatd  16538  clatleglb  17331  mrcmndind  17571  grpinveu  17661  dfgrp3lem  17718  issubg4  17815  gexdvds  18200  sylow2alem2  18234  obselocv  20282  scmatscm  20530  tgcn  21270  tgcnp  21271  lmconst  21279  cncls2  21291  cncls  21292  cnntr  21293  lmss  21316  cnt0  21364  isnrm2  21376  isreg2  21395  cmpsublem  21416  cmpsub  21417  tgcmp  21418  islly2  21501  kgencn2  21574  txdis  21649  txlm  21665  kqt0lem  21753  isr0  21754  regr1lem2  21757  cmphaushmeo  21817  cfinufil  21945  ufilen  21947  flimopn  21992  fbflim2  21994  fclsnei  22036  fclsbas  22038  fclsrest  22041  flimfnfcls  22045  fclscmp  22047  ufilcmp  22049  isfcf  22051  fcfnei  22052  cnpfcf  22058  tsmsres  22160  tsmsxp  22171  blbas  22448  prdsbl  22509  metss  22526  metcnp3  22558  bndth  22970  lebnumii  22978  iscfil3  23283  iscmet3lem1  23301  equivcfil  23309  equivcau  23310  ellimc3  23857  lhop1  23991  dvfsumrlim  24008  ftc1lem6  24018  fta1g  24141  dgrco  24245  plydivex  24266  fta1  24277  vieta1  24281  ulmshftlem  24357  ulmcaulem  24362  mtest  24372  cxpcn3lem  24702  cxploglim  24918  ftalem3  25015  dchrisumlem3  25394  pntibnd  25496  ostth2lem2  25537  grpoinveu  27702  nmcvcn  27878  blocnilem  27987  ubthlem3  28056  htthlem  28102  spansni  28744  bra11  29295  lmxrge0  30323  mrsubff1  31734  msubff1  31776  fnemeet2  32683  fnejoin2  32685  fin2so  33709  lindsenlbs  33717  poimirlem29  33751  poimirlem30  33752  ftc1cnnc  33796  incsequz2  33856  geomcau  33866  caushft  33868  sstotbnd2  33884  isbnd2  33893  totbndbnd  33899  ismtybndlem  33916  heibor  33931  atlatle  35100  cvlcvr1  35119  ltrnid  35915  ltrneq2  35928  climinf  40318  ralbinrald  41711  snlindsntorlem  42827
  Copyright terms: Public domain W3C validator