Theorem ralrimdva 3134

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3045

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 3046

This theorem is referenced by:  ralxfrd  5366  ralxfrd2  5370  isoselem  7319  resixpfo  8912  findcard  9133  ordtypelem2  9479  alephinit  10055  isfin2-2  10279  axpre-sup  11129  nnsub  12237  ublbneg  12899  xralrple  13172  supxrunb1  13286  expnlbnd2  14206  faclbnd4lem4  14268  hashbc  14425  cau3lem  15328  limsupbnd2  15456  climrlim2  15520  climshftlem  15547  subcn2  15568  isercoll  15641  climsup  15643  serf0  15654  iseralt  15658  incexclem  15809  sqrt2irr  16224  pclem  16816  prmpwdvds  16882  vdwlem10  16968  vdwlem13  16971  ramtlecl  16978  ramub  16991  ramcl  17007  iscatd  17641  clatleglb  18484  mndind  18762  grpinveu  18913  dfgrp3lem  18977  issubg4  19084  gexdvds  19521  sylow2alem2  19555  obselocv  21644  scmatscm  22407  tgcn  23146  tgcnp  23147  lmconst  23155  cncls2  23167  cncls  23168  cnntr  23169  lmss  23192  cnt0  23240  isnrm2  23252  isreg2  23271  cmpsublem  23293  cmpsub  23294  tgcmp  23295  islly2  23378  kgencn2  23451  txdis  23526  txlm  23542  kqt0lem  23630  isr0  23631  regr1lem2  23634  cmphaushmeo  23694  cfinufil  23822  ufilen  23824  flimopn  23869  fbflim2  23871  fclsnei  23913  fclsbas  23915  fclsrest  23918  flimfnfcls  23922  fclscmp  23924  ufilcmp  23926  isfcf  23928  fcfnei  23929  cnpfcf  23935  tsmsres  24038  tsmsxp  24049  blbas  24325  prdsbl  24386  metss  24403  metcnp3  24435  bndth  24864  lebnumii  24872  iscfil3  25180  iscmet3lem1  25198  equivcfil  25206  equivcau  25207  ellimc3  25787  lhop1  25926  dvfsumrlim  25945  ftc1lem6  25955  fta1g  26082  dgrco  26188  plydivex  26212  fta1  26223  vieta1  26227  ulmshftlem  26305  ulmcaulem  26310  mtest  26320  cxpcn3lem  26664  cxploglim  26895  ftalem3  26992  dchrisumlem3  27409  pntibnd  27511  ostth2lem2  27552  n0subs  28260  grpoinveu  30455  nmcvcn  30631  blocnilem  30740  ubthlem3  30808  htthlem  30853  spansni  31493  bra11  32044  lmxrge0  33949  mrsubff1  35508  msubff1  35550  fnemeet2  36362  fnejoin2  36364  fin2so  37608  lindsenlbs  37616  poimirlem29  37650  poimirlem30  37651  ftc1cnnc  37693  incsequz2  37750  geomcau  37760  caushft  37762  sstotbnd2  37775  isbnd2  37784  totbndbnd  37790  ismtybndlem  37807  heibor  37822  atlatle  39320  cvlcvr1  39339  ltrnid  40136  ltrneq2  40149  nadd1suc  43388  climinf  45611  ralbinrald  47127  snlindsntorlem  48463