Theorem ralrimdva 3151

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  ralxfrd  5413  ralxfrd2  5417  isoselem  7360  resixpfo  8974  findcard  9201  ordtypelem2  9556  alephinit  10132  isfin2-2  10356  axpre-sup  11206  nnsub  12307  ublbneg  12972  xralrple  13243  supxrunb1  13357  expnlbnd2  14269  faclbnd4lem4  14331  hashbc  14488  cau3lem  15389  limsupbnd2  15515  climrlim2  15579  climshftlem  15606  subcn2  15627  isercoll  15700  climsup  15702  serf0  15713  iseralt  15717  incexclem  15868  sqrt2irr  16281  pclem  16871  prmpwdvds  16937  vdwlem10  17023  vdwlem13  17026  ramtlecl  17033  ramub  17046  ramcl  17062  iscatd  17717  clatleglb  18575  mndind  18853  grpinveu  19004  dfgrp3lem  19068  issubg4  19175  gexdvds  19616  sylow2alem2  19650  obselocv  21765  scmatscm  22534  tgcn  23275  tgcnp  23276  lmconst  23284  cncls2  23296  cncls  23297  cnntr  23298  lmss  23321  cnt0  23369  isnrm2  23381  isreg2  23400  cmpsublem  23422  cmpsub  23423  tgcmp  23424  islly2  23507  kgencn2  23580  txdis  23655  txlm  23671  kqt0lem  23759  isr0  23760  regr1lem2  23763  cmphaushmeo  23823  cfinufil  23951  ufilen  23953  flimopn  23998  fbflim2  24000  fclsnei  24042  fclsbas  24044  fclsrest  24047  flimfnfcls  24051  fclscmp  24053  ufilcmp  24055  isfcf  24057  fcfnei  24058  cnpfcf  24064  tsmsres  24167  tsmsxp  24178  blbas  24455  prdsbl  24519  metss  24536  metcnp3  24568  bndth  25003  lebnumii  25011  iscfil3  25320  iscmet3lem1  25338  equivcfil  25346  equivcau  25347  ellimc3  25928  lhop1  26067  dvfsumrlim  26086  ftc1lem6  26096  fta1g  26223  dgrco  26329  plydivex  26353  fta1  26364  vieta1  26368  ulmshftlem  26446  ulmcaulem  26451  mtest  26461  cxpcn3lem  26804  cxploglim  27035  ftalem3  27132  dchrisumlem3  27549  pntibnd  27651  ostth2lem2  27692  n0subs  28374  grpoinveu  30547  nmcvcn  30723  blocnilem  30832  ubthlem3  30900  htthlem  30945  spansni  31585  bra11  32136  lmxrge0  33912  mrsubff1  35498  msubff1  35540  fnemeet2  36349  fnejoin2  36351  fin2so  37593  lindsenlbs  37601  poimirlem29  37635  poimirlem30  37636  ftc1cnnc  37678  incsequz2  37735  geomcau  37745  caushft  37747  sstotbnd2  37760  isbnd2  37769  totbndbnd  37775  ismtybndlem  37792  heibor  37807  atlatle  39301  cvlcvr1  39320  ltrnid  40117  ltrneq2  40130  nadd1suc  43381  climinf  45561  ralbinrald  47071  snlindsntorlem  48315