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  10024  isfin2-2  10248  axpre-sup  11098  nnsub  12206  ublbneg  12868  xralrple  13141  supxrunb1  13255  expnlbnd2  14175  faclbnd4lem4  14237  hashbc  14394  cau3lem  15297  limsupbnd2  15425  climrlim2  15489  climshftlem  15516  subcn2  15537  isercoll  15610  climsup  15612  serf0  15623  iseralt  15627  incexclem  15778  sqrt2irr  16193  pclem  16785  prmpwdvds  16851  vdwlem10  16937  vdwlem13  16940  ramtlecl  16947  ramub  16960  ramcl  16976  iscatd  17614  clatleglb  18459  mndind  18737  grpinveu  18888  dfgrp3lem  18952  issubg4  19059  gexdvds  19498  sylow2alem2  19532  obselocv  21670  scmatscm  22433  tgcn  23172  tgcnp  23173  lmconst  23181  cncls2  23193  cncls  23194  cnntr  23195  lmss  23218  cnt0  23266  isnrm2  23278  isreg2  23297  cmpsublem  23319  cmpsub  23320  tgcmp  23321  islly2  23404  kgencn2  23477  txdis  23552  txlm  23568  kqt0lem  23656  isr0  23657  regr1lem2  23660  cmphaushmeo  23720  cfinufil  23848  ufilen  23850  flimopn  23895  fbflim2  23897  fclsnei  23939  fclsbas  23941  fclsrest  23944  flimfnfcls  23948  fclscmp  23950  ufilcmp  23952  isfcf  23954  fcfnei  23955  cnpfcf  23961  tsmsres  24064  tsmsxp  24075  blbas  24351  prdsbl  24412  metss  24429  metcnp3  24461  bndth  24890  lebnumii  24898  iscfil3  25206  iscmet3lem1  25224  equivcfil  25232  equivcau  25233  ellimc3  25813  lhop1  25952  dvfsumrlim  25971  ftc1lem6  25981  fta1g  26108  dgrco  26214  plydivex  26238  fta1  26249  vieta1  26253  ulmshftlem  26331  ulmcaulem  26336  mtest  26346  cxpcn3lem  26690  cxploglim  26921  ftalem3  27018  dchrisumlem3  27435  pntibnd  27537  ostth2lem2  27578  n0subs  28293  grpoinveu  30498  nmcvcn  30674  blocnilem  30783  ubthlem3  30851  htthlem  30896  spansni  31536  bra11  32087  lmxrge0  33935  mrsubff1  35494  msubff1  35536  fnemeet2  36348  fnejoin2  36350  fin2so  37594  lindsenlbs  37602  poimirlem29  37636  poimirlem30  37637  ftc1cnnc  37679  incsequz2  37736  geomcau  37746  caushft  37748  sstotbnd2  37761  isbnd2  37770  totbndbnd  37776  ismtybndlem  37793  heibor  37808  atlatle  39306  cvlcvr1  39325  ltrnid  40122  ltrneq2  40135  nadd1suc  43374  climinf  45597  ralbinrald  47116  snlindsntorlem  48452