Theorem ralrimdva 3133

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

Step	Hyp	Ref	Expression
1		ralrimdva.1	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
2	1	expimpd 453	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒))
3	2	expcomd 416	. 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralrimdv 3131	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  ralxfrd  5358  ralxfrd2  5362  isoselem  7298  resixpfo  8886  findcard  9104  ordtypelem2  9448  alephinit  10026  isfin2-2  10250  axpre-sup  11100  nnsub  12208  ublbneg  12870  xralrple  13143  supxrunb1  13257  expnlbnd2  14177  faclbnd4lem4  14239  hashbc  14396  cau3lem  15298  limsupbnd2  15426  climrlim2  15490  climshftlem  15517  subcn2  15538  isercoll  15611  climsup  15613  serf0  15624  iseralt  15628  incexclem  15779  sqrt2irr  16194  pclem  16786  prmpwdvds  16852  vdwlem10  16938  vdwlem13  16941  ramtlecl  16948  ramub  16961  ramcl  16977  iscatd  17615  clatleglb  18460  mndind  18738  grpinveu  18889  dfgrp3lem  18953  issubg4  19060  gexdvds  19499  sylow2alem2  19533  obselocv  21671  scmatscm  22434  tgcn  23173  tgcnp  23174  lmconst  23182  cncls2  23194  cncls  23195  cnntr  23196  lmss  23219  cnt0  23267  isnrm2  23279  isreg2  23298  cmpsublem  23320  cmpsub  23321  tgcmp  23322  islly2  23405  kgencn2  23478  txdis  23553  txlm  23569  kqt0lem  23657  isr0  23658  regr1lem2  23661  cmphaushmeo  23721  cfinufil  23849  ufilen  23851  flimopn  23896  fbflim2  23898  fclsnei  23940  fclsbas  23942  fclsrest  23945  flimfnfcls  23949  fclscmp  23951  ufilcmp  23953  isfcf  23955  fcfnei  23956  cnpfcf  23962  tsmsres  24065  tsmsxp  24076  blbas  24352  prdsbl  24413  metss  24430  metcnp3  24462  bndth  24891  lebnumii  24899  iscfil3  25207  iscmet3lem1  25225  equivcfil  25233  equivcau  25234  ellimc3  25814  lhop1  25953  dvfsumrlim  25972  ftc1lem6  25982  fta1g  26109  dgrco  26215  plydivex  26239  fta1  26250  vieta1  26254  ulmshftlem  26332  ulmcaulem  26337  mtest  26347  cxpcn3lem  26691  cxploglim  26922  ftalem3  27019  dchrisumlem3  27436  pntibnd  27538  ostth2lem2  27579  n0subs  28294  grpoinveu  30499  nmcvcn  30675  blocnilem  30784  ubthlem3  30852  htthlem  30897  spansni  31537  bra11  32088  lmxrge0  33936  mrsubff1  35495  msubff1  35537  fnemeet2  36349  fnejoin2  36351  fin2so  37595  lindsenlbs  37603  poimirlem29  37637  poimirlem30  37638  ftc1cnnc  37680  incsequz2  37737  geomcau  37747  caushft  37749  sstotbnd2  37762  isbnd2  37771  totbndbnd  37777  ismtybndlem  37794  heibor  37809  atlatle  39307  cvlcvr1  39326  ltrnid  40123  ltrneq2  40136  nadd1suc  43375  climinf  45598  ralbinrald  47117  snlindsntorlem  48453