Theorem ralrimdva 3140

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 3138	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051

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 3052

This theorem is referenced by:  ralxfrd  5378  ralxfrd2  5382  isoselem  7333  resixpfo  8948  findcard  9175  ordtypelem2  9531  alephinit  10107  isfin2-2  10331  axpre-sup  11181  nnsub  12282  ublbneg  12947  xralrple  13219  supxrunb1  13333  expnlbnd2  14250  faclbnd4lem4  14312  hashbc  14469  cau3lem  15371  limsupbnd2  15497  climrlim2  15561  climshftlem  15588  subcn2  15609  isercoll  15682  climsup  15684  serf0  15695  iseralt  15699  incexclem  15850  sqrt2irr  16265  pclem  16856  prmpwdvds  16922  vdwlem10  17008  vdwlem13  17011  ramtlecl  17018  ramub  17031  ramcl  17047  iscatd  17683  clatleglb  18526  mndind  18804  grpinveu  18955  dfgrp3lem  19019  issubg4  19126  gexdvds  19563  sylow2alem2  19597  obselocv  21686  scmatscm  22449  tgcn  23188  tgcnp  23189  lmconst  23197  cncls2  23209  cncls  23210  cnntr  23211  lmss  23234  cnt0  23282  isnrm2  23294  isreg2  23313  cmpsublem  23335  cmpsub  23336  tgcmp  23337  islly2  23420  kgencn2  23493  txdis  23568  txlm  23584  kqt0lem  23672  isr0  23673  regr1lem2  23676  cmphaushmeo  23736  cfinufil  23864  ufilen  23866  flimopn  23911  fbflim2  23913  fclsnei  23955  fclsbas  23957  fclsrest  23960  flimfnfcls  23964  fclscmp  23966  ufilcmp  23968  isfcf  23970  fcfnei  23971  cnpfcf  23977  tsmsres  24080  tsmsxp  24091  blbas  24367  prdsbl  24428  metss  24445  metcnp3  24477  bndth  24906  lebnumii  24914  iscfil3  25223  iscmet3lem1  25241  equivcfil  25249  equivcau  25250  ellimc3  25830  lhop1  25969  dvfsumrlim  25988  ftc1lem6  25998  fta1g  26125  dgrco  26231  plydivex  26255  fta1  26266  vieta1  26270  ulmshftlem  26348  ulmcaulem  26353  mtest  26363  cxpcn3lem  26707  cxploglim  26938  ftalem3  27035  dchrisumlem3  27452  pntibnd  27554  ostth2lem2  27595  n0subs  28277  grpoinveu  30446  nmcvcn  30622  blocnilem  30731  ubthlem3  30799  htthlem  30844  spansni  31484  bra11  32035  lmxrge0  33929  mrsubff1  35482  msubff1  35524  fnemeet2  36331  fnejoin2  36333  fin2so  37577  lindsenlbs  37585  poimirlem29  37619  poimirlem30  37620  ftc1cnnc  37662  incsequz2  37719  geomcau  37729  caushft  37731  sstotbnd2  37744  isbnd2  37753  totbndbnd  37759  ismtybndlem  37776  heibor  37791  atlatle  39284  cvlcvr1  39303  ltrnid  40100  ltrneq2  40113  nadd1suc  43363  climinf  45583  ralbinrald  47099  snlindsntorlem  48394