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

Theorem ralrimdva 3183
 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 457 . . 3 (𝜑 → ((𝑥𝐴𝜓) → 𝜒))
32expcomd 420 . 2 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
43ralrimdv 3182 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2115  ∀wral 3132 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912 This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3137 This theorem is referenced by:  ralxfrd  5292  ralxfrd2  5296  isoselem  7078  resixpfo  8485  findcard  8743  ordtypelem2  8969  alephinit  9508  isfin2-2  9728  axpre-sup  10578  nnsub  11669  ublbneg  12321  xralrple  12586  supxrunb1  12700  expnlbnd2  13591  faclbnd4lem4  13652  hashbc  13807  cau3lem  14705  limsupbnd2  14831  climrlim2  14895  climshftlem  14922  subcn2  14942  isercoll  15015  climsup  15017  serf0  15028  iseralt  15032  incexclem  15182  sqrt2irr  15593  pclem  16164  prmpwdvds  16229  vdwlem10  16315  vdwlem13  16318  ramtlecl  16325  ramub  16338  ramcl  16354  iscatd  16935  clatleglb  17727  mndind  17983  grpinveu  18129  dfgrp3lem  18188  issubg4  18289  gexdvds  18700  sylow2alem2  18734  obselocv  20860  scmatscm  21110  tgcn  21848  tgcnp  21849  lmconst  21857  cncls2  21869  cncls  21870  cnntr  21871  lmss  21894  cnt0  21942  isnrm2  21954  isreg2  21973  cmpsublem  21995  cmpsub  21996  tgcmp  21997  islly2  22080  kgencn2  22153  txdis  22228  txlm  22244  kqt0lem  22332  isr0  22333  regr1lem2  22336  cmphaushmeo  22396  cfinufil  22524  ufilen  22526  flimopn  22571  fbflim2  22573  fclsnei  22615  fclsbas  22617  fclsrest  22620  flimfnfcls  22624  fclscmp  22626  ufilcmp  22628  isfcf  22630  fcfnei  22631  cnpfcf  22637  tsmsres  22740  tsmsxp  22751  blbas  23028  prdsbl  23089  metss  23106  metcnp3  23138  bndth  23554  lebnumii  23562  iscfil3  23868  iscmet3lem1  23886  equivcfil  23894  equivcau  23895  ellimc3  24473  lhop1  24608  dvfsumrlim  24625  ftc1lem6  24635  fta1g  24759  dgrco  24863  plydivex  24884  fta1  24895  vieta1  24899  ulmshftlem  24975  ulmcaulem  24980  mtest  24990  cxpcn3lem  25327  cxploglim  25554  ftalem3  25651  dchrisumlem3  26066  pntibnd  26168  ostth2lem2  26209  grpoinveu  28293  nmcvcn  28469  blocnilem  28578  ubthlem3  28646  htthlem  28691  spansni  29331  bra11  29882  lmxrge0  31215  mrsubff1  32781  msubff1  32823  fnemeet2  33735  fnejoin2  33737  fin2so  34949  lindsenlbs  34957  poimirlem29  34991  poimirlem30  34992  ftc1cnnc  35034  incsequz2  35092  geomcau  35102  caushft  35104  sstotbnd2  35117  isbnd2  35126  totbndbnd  35132  ismtybndlem  35149  heibor  35164  atlatle  36521  cvlcvr1  36540  ltrnid  37336  ltrneq2  37349  climinf  42105  ralbinrald  43535  snlindsntorlem  44735
 Copyright terms: Public domain W3C validator