Theorem ralrimdva 3141

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-an 398  df-ral 3056

This theorem is referenced by:  ralxfrd  5340  ralxfrd2  5344  isoselem  7289  resixpfo  8878  findcard  9092  ordtypelem2  9428  alephinit  10012  isfin2-2  10236  axpre-sup  11087  nnsub  12216  ublbneg  12878  xralrple  13152  supxrunb1  13266  expnlbnd2  14191  faclbnd4lem4  14253  hashbc  14410  cau3lem  15312  limsupbnd2  15440  climrlim2  15504  climshftlem  15531  subcn2  15552  isercoll  15625  climsup  15627  serf0  15638  iseralt  15642  incexclem  15796  sqrt2irr  16211  pclem  16804  prmpwdvds  16870  vdwlem10  16956  vdwlem13  16959  ramtlecl  16966  ramub  16979  ramcl  16995  iscatd  17634  clatleglb  18479  mndind  18791  grpinveu  18945  dfgrp3lem  19009  issubg4  19116  gexdvds  19554  sylow2alem2  19588  obselocv  21707  scmatscm  22500  tgcn  23239  tgcnp  23240  lmconst  23248  cncls2  23260  cncls  23261  cnntr  23262  lmss  23285  cnt0  23333  isnrm2  23345  isreg2  23364  cmpsublem  23386  cmpsub  23387  tgcmp  23388  islly2  23471  kgencn2  23544  txdis  23619  txlm  23635  kqt0lem  23723  isr0  23724  regr1lem2  23727  cmphaushmeo  23787  cfinufil  23915  ufilen  23917  flimopn  23962  fbflim2  23964  fclsnei  24006  fclsbas  24008  fclsrest  24011  flimfnfcls  24015  fclscmp  24017  ufilcmp  24019  isfcf  24021  fcfnei  24022  cnpfcf  24028  tsmsres  24131  tsmsxp  24142  blbas  24417  prdsbl  24478  metss  24495  metcnp3  24527  bndth  24947  lebnumii  24955  iscfil3  25262  iscmet3lem1  25280  equivcfil  25288  equivcau  25289  ellimc3  25868  lhop1  26003  dvfsumrlim  26020  ftc1lem6  26030  fta1g  26157  dgrco  26262  plydivex  26285  fta1  26296  vieta1  26300  ulmshftlem  26376  ulmcaulem  26381  mtest  26391  cxpcn3lem  26733  cxploglim  26963  ftalem3  27060  dchrisumlem3  27476  pntibnd  27578  ostth2lem2  27619  n0subs  28377  grpoinveu  30612  nmcvcn  30788  blocnilem  30897  ubthlem3  30965  htthlem  31010  spansni  31650  bra11  32201  lmxrge0  34148  mrsubff1  35757  msubff1  35799  fnemeet2  36610  fnejoin2  36612  fin2so  37989  lindsenlbs  37997  poimirlem29  38031  poimirlem30  38032  ftc1cnnc  38074  incsequz2  38131  geomcau  38141  caushft  38143  sstotbnd2  38156  isbnd2  38165  totbndbnd  38171  ismtybndlem  38188  heibor  38203  atlatle  39827  cvlcvr1  39846  ltrnid  40642  ltrneq2  40655  nadd1suc  43852  climinf  46065  ralbinrald  47599  snlindsntorlem  48975