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

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

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 3062

This theorem is referenced by:  ralxfrd  5408  ralxfrd2  5412  isoselem  7361  resixpfo  8976  findcard  9203  ordtypelem2  9559  alephinit  10135  isfin2-2  10359  axpre-sup  11209  nnsub  12310  ublbneg  12975  xralrple  13247  supxrunb1  13361  expnlbnd2  14273  faclbnd4lem4  14335  hashbc  14492  cau3lem  15393  limsupbnd2  15519  climrlim2  15583  climshftlem  15610  subcn2  15631  isercoll  15704  climsup  15706  serf0  15717  iseralt  15721  incexclem  15872  sqrt2irr  16285  pclem  16876  prmpwdvds  16942  vdwlem10  17028  vdwlem13  17031  ramtlecl  17038  ramub  17051  ramcl  17067  iscatd  17716  clatleglb  18563  mndind  18841  grpinveu  18992  dfgrp3lem  19056  issubg4  19163  gexdvds  19602  sylow2alem2  19636  obselocv  21748  scmatscm  22519  tgcn  23260  tgcnp  23261  lmconst  23269  cncls2  23281  cncls  23282  cnntr  23283  lmss  23306  cnt0  23354  isnrm2  23366  isreg2  23385  cmpsublem  23407  cmpsub  23408  tgcmp  23409  islly2  23492  kgencn2  23565  txdis  23640  txlm  23656  kqt0lem  23744  isr0  23745  regr1lem2  23748  cmphaushmeo  23808  cfinufil  23936  ufilen  23938  flimopn  23983  fbflim2  23985  fclsnei  24027  fclsbas  24029  fclsrest  24032  flimfnfcls  24036  fclscmp  24038  ufilcmp  24040  isfcf  24042  fcfnei  24043  cnpfcf  24049  tsmsres  24152  tsmsxp  24163  blbas  24440  prdsbl  24504  metss  24521  metcnp3  24553  bndth  24990  lebnumii  24998  iscfil3  25307  iscmet3lem1  25325  equivcfil  25333  equivcau  25334  ellimc3  25914  lhop1  26053  dvfsumrlim  26072  ftc1lem6  26082  fta1g  26209  dgrco  26315  plydivex  26339  fta1  26350  vieta1  26354  ulmshftlem  26432  ulmcaulem  26437  mtest  26447  cxpcn3lem  26790  cxploglim  27021  ftalem3  27118  dchrisumlem3  27535  pntibnd  27637  ostth2lem2  27678  n0subs  28360  grpoinveu  30538  nmcvcn  30714  blocnilem  30823  ubthlem3  30891  htthlem  30936  spansni  31576  bra11  32127  lmxrge0  33951  mrsubff1  35519  msubff1  35561  fnemeet2  36368  fnejoin2  36370  fin2so  37614  lindsenlbs  37622  poimirlem29  37656  poimirlem30  37657  ftc1cnnc  37699  incsequz2  37756  geomcau  37766  caushft  37768  sstotbnd2  37781  isbnd2  37790  totbndbnd  37796  ismtybndlem  37813  heibor  37828  atlatle  39321  cvlcvr1  39340  ltrnid  40137  ltrneq2  40150  nadd1suc  43405  climinf  45621  ralbinrald  47134  snlindsntorlem  48387