Theorem ralrimdva 3138

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

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

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 3053

This theorem is referenced by:  ralxfrd  5357  ralxfrd2  5361  isoselem  7299  resixpfo  8888  findcard  9102  ordtypelem2  9438  alephinit  10019  isfin2-2  10243  axpre-sup  11094  nnsub  12203  ublbneg  12860  xralrple  13134  supxrunb1  13248  expnlbnd2  14171  faclbnd4lem4  14233  hashbc  14390  cau3lem  15292  limsupbnd2  15420  climrlim2  15484  climshftlem  15511  subcn2  15532  isercoll  15605  climsup  15607  serf0  15618  iseralt  15622  incexclem  15773  sqrt2irr  16188  pclem  16780  prmpwdvds  16846  vdwlem10  16932  vdwlem13  16935  ramtlecl  16942  ramub  16955  ramcl  16971  iscatd  17610  clatleglb  18455  mndind  18767  grpinveu  18921  dfgrp3lem  18985  issubg4  19092  gexdvds  19530  sylow2alem2  19564  obselocv  21700  scmatscm  22474  tgcn  23213  tgcnp  23214  lmconst  23222  cncls2  23234  cncls  23235  cnntr  23236  lmss  23259  cnt0  23307  isnrm2  23319  isreg2  23338  cmpsublem  23360  cmpsub  23361  tgcmp  23362  islly2  23445  kgencn2  23518  txdis  23593  txlm  23609  kqt0lem  23697  isr0  23698  regr1lem2  23701  cmphaushmeo  23761  cfinufil  23889  ufilen  23891  flimopn  23936  fbflim2  23938  fclsnei  23980  fclsbas  23982  fclsrest  23985  flimfnfcls  23989  fclscmp  23991  ufilcmp  23993  isfcf  23995  fcfnei  23996  cnpfcf  24002  tsmsres  24105  tsmsxp  24116  blbas  24391  prdsbl  24452  metss  24469  metcnp3  24501  bndth  24930  lebnumii  24938  iscfil3  25246  iscmet3lem1  25264  equivcfil  25272  equivcau  25273  ellimc3  25853  lhop1  25992  dvfsumrlim  26011  ftc1lem6  26021  fta1g  26148  dgrco  26254  plydivex  26278  fta1  26289  vieta1  26293  ulmshftlem  26371  ulmcaulem  26376  mtest  26386  cxpcn3lem  26730  cxploglim  26961  ftalem3  27058  dchrisumlem3  27475  pntibnd  27577  ostth2lem2  27618  n0subs  28376  grpoinveu  30613  nmcvcn  30789  blocnilem  30898  ubthlem3  30966  htthlem  31011  spansni  31651  bra11  32202  lmxrge0  34136  mrsubff1  35736  msubff1  35778  fnemeet2  36589  fnejoin2  36591  fin2so  37887  lindsenlbs  37895  poimirlem29  37929  poimirlem30  37930  ftc1cnnc  37972  incsequz2  38029  geomcau  38039  caushft  38041  sstotbnd2  38054  isbnd2  38063  totbndbnd  38069  ismtybndlem  38086  heibor  38101  atlatle  39725  cvlcvr1  39744  ltrnid  40540  ltrneq2  40553  nadd1suc  43778  climinf  45995  ralbinrald  47511  snlindsntorlem  48859