Theorem ralrimdva 3132

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralxfrd  5344  ralxfrd2  5348  isoselem  7275  resixpfo  8860  findcard  9073  ordtypelem2  9405  alephinit  9986  isfin2-2  10210  axpre-sup  11060  nnsub  12169  ublbneg  12831  xralrple  13104  supxrunb1  13218  expnlbnd2  14141  faclbnd4lem4  14203  hashbc  14360  cau3lem  15262  limsupbnd2  15390  climrlim2  15454  climshftlem  15481  subcn2  15502  isercoll  15575  climsup  15577  serf0  15588  iseralt  15592  incexclem  15743  sqrt2irr  16158  pclem  16750  prmpwdvds  16816  vdwlem10  16902  vdwlem13  16905  ramtlecl  16912  ramub  16925  ramcl  16941  iscatd  17579  clatleglb  18424  mndind  18736  grpinveu  18887  dfgrp3lem  18951  issubg4  19058  gexdvds  19496  sylow2alem2  19530  obselocv  21665  scmatscm  22428  tgcn  23167  tgcnp  23168  lmconst  23176  cncls2  23188  cncls  23189  cnntr  23190  lmss  23213  cnt0  23261  isnrm2  23273  isreg2  23292  cmpsublem  23314  cmpsub  23315  tgcmp  23316  islly2  23399  kgencn2  23472  txdis  23547  txlm  23563  kqt0lem  23651  isr0  23652  regr1lem2  23655  cmphaushmeo  23715  cfinufil  23843  ufilen  23845  flimopn  23890  fbflim2  23892  fclsnei  23934  fclsbas  23936  fclsrest  23939  flimfnfcls  23943  fclscmp  23945  ufilcmp  23947  isfcf  23949  fcfnei  23950  cnpfcf  23956  tsmsres  24059  tsmsxp  24070  blbas  24345  prdsbl  24406  metss  24423  metcnp3  24455  bndth  24884  lebnumii  24892  iscfil3  25200  iscmet3lem1  25218  equivcfil  25226  equivcau  25227  ellimc3  25807  lhop1  25946  dvfsumrlim  25965  ftc1lem6  25975  fta1g  26102  dgrco  26208  plydivex  26232  fta1  26243  vieta1  26247  ulmshftlem  26325  ulmcaulem  26330  mtest  26340  cxpcn3lem  26684  cxploglim  26915  ftalem3  27012  dchrisumlem3  27429  pntibnd  27531  ostth2lem2  27572  n0subs  28289  grpoinveu  30499  nmcvcn  30675  blocnilem  30784  ubthlem3  30852  htthlem  30897  spansni  31537  bra11  32088  lmxrge0  33965  mrsubff1  35558  msubff1  35600  fnemeet2  36411  fnejoin2  36413  fin2so  37646  lindsenlbs  37654  poimirlem29  37688  poimirlem30  37689  ftc1cnnc  37731  incsequz2  37788  geomcau  37798  caushft  37800  sstotbnd2  37813  isbnd2  37822  totbndbnd  37828  ismtybndlem  37845  heibor  37860  atlatle  39418  cvlcvr1  39437  ltrnid  40233  ltrneq2  40246  nadd1suc  43484  climinf  45705  ralbinrald  47221  snlindsntorlem  48570