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

Theorem ralrimdva 3095
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 630 . . 3 (𝜑 → ((𝑥𝐴𝜓) → 𝜒))
32expcomd 453 . 2 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
43ralrimdv 3094 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2127  wral 3038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976
This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3043
This theorem is referenced by:  ralxfrd  5016  ralxfrdOLD  5017  ralxfrd2  5021  isoselem  6742  resixpfo  8100  findcard  8352  ordtypelem2  8577  alephinit  9079  isfin2-2  9304  axpre-sup  10153  nnsub  11222  ublbneg  11937  xralrple  12200  supxrunb1  12313  expnlbnd2  13160  faclbnd4lem4  13248  hashbc  13400  cau3lem  14264  limsupbnd2  14384  climrlim2  14448  climshftlem  14475  subcn2  14495  isercoll  14568  climsup  14570  serf0  14581  iseralt  14585  incexclem  14738  sqrt2irr  15149  pclem  15716  prmpwdvds  15781  vdwlem10  15867  vdwlem13  15870  ramtlecl  15877  ramub  15890  ramcl  15906  iscatd  16506  clatleglb  17298  mrcmndind  17538  grpinveu  17628  dfgrp3lem  17685  issubg4  17785  gexdvds  18170  sylow2alem2  18204  obselocv  20245  scmatscm  20492  tgcn  21229  tgcnp  21230  lmconst  21238  cncls2  21250  cncls  21251  cnntr  21252  lmss  21275  cnt0  21323  isnrm2  21335  isreg2  21354  cmpsublem  21375  cmpsub  21376  tgcmp  21377  islly2  21460  kgencn2  21533  txdis  21608  txlm  21624  kqt0lem  21712  isr0  21713  regr1lem2  21716  cmphaushmeo  21776  cfinufil  21904  ufilen  21906  flimopn  21951  fbflim2  21953  fclsnei  21995  fclsbas  21997  fclsrest  22000  flimfnfcls  22004  fclscmp  22006  ufilcmp  22008  isfcf  22010  fcfnei  22011  cnpfcf  22017  tsmsres  22119  tsmsxp  22130  blbas  22407  prdsbl  22468  metss  22485  metcnp3  22517  bndth  22929  lebnumii  22937  iscfil3  23242  iscmet3lem1  23260  equivcfil  23268  equivcau  23269  ellimc3  23813  lhop1  23947  dvfsumrlim  23964  ftc1lem6  23974  fta1g  24097  dgrco  24201  plydivex  24222  fta1  24233  vieta1  24237  ulmshftlem  24313  ulmcaulem  24318  mtest  24328  cxpcn3lem  24658  cxploglim  24874  ftalem3  24971  dchrisumlem3  25350  pntibnd  25452  ostth2lem2  25493  grpoinveu  27653  nmcvcn  27830  blocnilem  27939  ubthlem3  28008  htthlem  28054  spansni  28696  bra11  29247  lmxrge0  30278  mrsubff1  31689  msubff1  31731  fnemeet2  32639  fnejoin2  32641  fin2so  33678  lindsenlbs  33686  poimirlem29  33720  poimirlem30  33721  ftc1cnnc  33766  incsequz2  33827  geomcau  33837  caushft  33839  sstotbnd2  33855  isbnd2  33864  totbndbnd  33870  ismtybndlem  33887  heibor  33902  atlatle  35079  cvlcvr1  35098  ltrnid  35893  ltrneq2  35906  climinf  40310  ralbinrald  41674  snlindsntorlem  42738
  Copyright terms: Public domain W3C validator