Theorem ralrimdva 3137

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

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

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  ralxfrd  5350  ralxfrd2  5354  isoselem  7296  resixpfo  8884  findcard  9098  ordtypelem2  9434  alephinit  10017  isfin2-2  10241  axpre-sup  11092  nnsub  12221  ublbneg  12883  xralrple  13157  supxrunb1  13271  expnlbnd2  14196  faclbnd4lem4  14258  hashbc  14415  cau3lem  15317  limsupbnd2  15445  climrlim2  15509  climshftlem  15536  subcn2  15557  isercoll  15630  climsup  15632  serf0  15643  iseralt  15647  incexclem  15801  sqrt2irr  16216  pclem  16809  prmpwdvds  16875  vdwlem10  16961  vdwlem13  16964  ramtlecl  16971  ramub  16984  ramcl  17000  iscatd  17639  clatleglb  18484  mndind  18796  grpinveu  18950  dfgrp3lem  19014  issubg4  19121  gexdvds  19559  sylow2alem2  19593  obselocv  21708  scmatscm  22478  tgcn  23217  tgcnp  23218  lmconst  23226  cncls2  23238  cncls  23239  cnntr  23240  lmss  23263  cnt0  23311  isnrm2  23323  isreg2  23342  cmpsublem  23364  cmpsub  23365  tgcmp  23366  islly2  23449  kgencn2  23522  txdis  23597  txlm  23613  kqt0lem  23701  isr0  23702  regr1lem2  23705  cmphaushmeo  23765  cfinufil  23893  ufilen  23895  flimopn  23940  fbflim2  23942  fclsnei  23984  fclsbas  23986  fclsrest  23989  flimfnfcls  23993  fclscmp  23995  ufilcmp  23997  isfcf  23999  fcfnei  24000  cnpfcf  24006  tsmsres  24109  tsmsxp  24120  blbas  24395  prdsbl  24456  metss  24473  metcnp3  24505  bndth  24925  lebnumii  24933  iscfil3  25240  iscmet3lem1  25258  equivcfil  25266  equivcau  25267  ellimc3  25846  lhop1  25981  dvfsumrlim  25998  ftc1lem6  26008  fta1g  26135  dgrco  26240  plydivex  26263  fta1  26274  vieta1  26278  ulmshftlem  26354  ulmcaulem  26359  mtest  26369  cxpcn3lem  26711  cxploglim  26941  ftalem3  27038  dchrisumlem3  27454  pntibnd  27556  ostth2lem2  27597  n0subs  28355  grpoinveu  30590  nmcvcn  30766  blocnilem  30875  ubthlem3  30943  htthlem  30988  spansni  31628  bra11  32179  lmxrge0  34096  mrsubff1  35696  msubff1  35738  fnemeet2  36549  fnejoin2  36551  fin2so  37928  lindsenlbs  37936  poimirlem29  37970  poimirlem30  37971  ftc1cnnc  38013  incsequz2  38070  geomcau  38080  caushft  38082  sstotbnd2  38095  isbnd2  38104  totbndbnd  38110  ismtybndlem  38127  heibor  38142  atlatle  39766  cvlcvr1  39785  ltrnid  40581  ltrneq2  40594  nadd1suc  43820  climinf  46036  ralbinrald  47570  snlindsntorlem  48946