Theorem ralrimdva 3154

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 457	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒))
3	2	expcomd 420	. 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralrimdv 3153	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  ralxfrd  5274  ralxfrd2  5278  isoselem  7073  resixpfo  8483  findcard  8741  ordtypelem2  8967  alephinit  9506  isfin2-2  9730  axpre-sup  10580  nnsub  11669  ublbneg  12321  xralrple  12586  supxrunb1  12700  expnlbnd2  13591  faclbnd4lem4  13652  hashbc  13807  cau3lem  14706  limsupbnd2  14832  climrlim2  14896  climshftlem  14923  subcn2  14943  isercoll  15016  climsup  15018  serf0  15029  iseralt  15033  incexclem  15183  sqrt2irr  15594  pclem  16165  prmpwdvds  16230  vdwlem10  16316  vdwlem13  16319  ramtlecl  16326  ramub  16339  ramcl  16355  iscatd  16936  clatleglb  17728  mndind  17984  grpinveu  18130  dfgrp3lem  18189  issubg4  18290  gexdvds  18701  sylow2alem2  18735  obselocv  20417  scmatscm  21118  tgcn  21857  tgcnp  21858  lmconst  21866  cncls2  21878  cncls  21879  cnntr  21880  lmss  21903  cnt0  21951  isnrm2  21963  isreg2  21982  cmpsublem  22004  cmpsub  22005  tgcmp  22006  islly2  22089  kgencn2  22162  txdis  22237  txlm  22253  kqt0lem  22341  isr0  22342  regr1lem2  22345  cmphaushmeo  22405  cfinufil  22533  ufilen  22535  flimopn  22580  fbflim2  22582  fclsnei  22624  fclsbas  22626  fclsrest  22629  flimfnfcls  22633  fclscmp  22635  ufilcmp  22637  isfcf  22639  fcfnei  22640  cnpfcf  22646  tsmsres  22749  tsmsxp  22760  blbas  23037  prdsbl  23098  metss  23115  metcnp3  23147  bndth  23563  lebnumii  23571  iscfil3  23877  iscmet3lem1  23895  equivcfil  23903  equivcau  23904  ellimc3  24482  lhop1  24617  dvfsumrlim  24634  ftc1lem6  24644  fta1g  24768  dgrco  24872  plydivex  24893  fta1  24904  vieta1  24908  ulmshftlem  24984  ulmcaulem  24989  mtest  24999  cxpcn3lem  25336  cxploglim  25563  ftalem3  25660  dchrisumlem3  26075  pntibnd  26177  ostth2lem2  26218  grpoinveu  28302  nmcvcn  28478  blocnilem  28587  ubthlem3  28655  htthlem  28700  spansni  29340  bra11  29891  lmxrge0  31305  mrsubff1  32874  msubff1  32916  fnemeet2  33828  fnejoin2  33830  fin2so  35044  lindsenlbs  35052  poimirlem29  35086  poimirlem30  35087  ftc1cnnc  35129  incsequz2  35187  geomcau  35197  caushft  35199  sstotbnd2  35212  isbnd2  35221  totbndbnd  35227  ismtybndlem  35244  heibor  35259  atlatle  36616  cvlcvr1  36635  ltrnid  37431  ltrneq2  37444  climinf  42248  ralbinrald  43678  snlindsntorlem  44879