Theorem ralrimdva 3133

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

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

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 3045

This theorem is referenced by:  ralxfrd  5363  ralxfrd2  5367  isoselem  7316  resixpfo  8909  findcard  9127  ordtypelem2  9472  alephinit  10048  isfin2-2  10272  axpre-sup  11122  nnsub  12230  ublbneg  12892  xralrple  13165  supxrunb1  13279  expnlbnd2  14199  faclbnd4lem4  14261  hashbc  14418  cau3lem  15321  limsupbnd2  15449  climrlim2  15513  climshftlem  15540  subcn2  15561  isercoll  15634  climsup  15636  serf0  15647  iseralt  15651  incexclem  15802  sqrt2irr  16217  pclem  16809  prmpwdvds  16875  vdwlem10  16961  vdwlem13  16964  ramtlecl  16971  ramub  16984  ramcl  17000  iscatd  17634  clatleglb  18477  mndind  18755  grpinveu  18906  dfgrp3lem  18970  issubg4  19077  gexdvds  19514  sylow2alem2  19548  obselocv  21637  scmatscm  22400  tgcn  23139  tgcnp  23140  lmconst  23148  cncls2  23160  cncls  23161  cnntr  23162  lmss  23185  cnt0  23233  isnrm2  23245  isreg2  23264  cmpsublem  23286  cmpsub  23287  tgcmp  23288  islly2  23371  kgencn2  23444  txdis  23519  txlm  23535  kqt0lem  23623  isr0  23624  regr1lem2  23627  cmphaushmeo  23687  cfinufil  23815  ufilen  23817  flimopn  23862  fbflim2  23864  fclsnei  23906  fclsbas  23908  fclsrest  23911  flimfnfcls  23915  fclscmp  23917  ufilcmp  23919  isfcf  23921  fcfnei  23922  cnpfcf  23928  tsmsres  24031  tsmsxp  24042  blbas  24318  prdsbl  24379  metss  24396  metcnp3  24428  bndth  24857  lebnumii  24865  iscfil3  25173  iscmet3lem1  25191  equivcfil  25199  equivcau  25200  ellimc3  25780  lhop1  25919  dvfsumrlim  25938  ftc1lem6  25948  fta1g  26075  dgrco  26181  plydivex  26205  fta1  26216  vieta1  26220  ulmshftlem  26298  ulmcaulem  26303  mtest  26313  cxpcn3lem  26657  cxploglim  26888  ftalem3  26985  dchrisumlem3  27402  pntibnd  27504  ostth2lem2  27545  n0subs  28253  grpoinveu  30448  nmcvcn  30624  blocnilem  30733  ubthlem3  30801  htthlem  30846  spansni  31486  bra11  32037  lmxrge0  33942  mrsubff1  35501  msubff1  35543  fnemeet2  36355  fnejoin2  36357  fin2so  37601  lindsenlbs  37609  poimirlem29  37643  poimirlem30  37644  ftc1cnnc  37686  incsequz2  37743  geomcau  37753  caushft  37755  sstotbnd2  37768  isbnd2  37777  totbndbnd  37783  ismtybndlem  37800  heibor  37815  atlatle  39313  cvlcvr1  39332  ltrnid  40129  ltrneq2  40142  nadd1suc  43381  climinf  45604  ralbinrald  47123  snlindsntorlem  48459