Theorem ralrimdva 3171

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 458	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒))
3	2	expcomd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))
4	3	ralrimdv 3169	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  ralxfrd  5380  ralxfrd2  5384  isoselem  7340  resixpfo  8934  findcard  9148  ordtypelem2  9481  alephinit  10079  isfin2-2  10303  axpre-sup  11154  nnsub  12280  ublbneg  12957  xralrple  13231  supxrunb1  13345  expnlbnd2  14270  faclbnd4lem4  14332  hashbc  14490  cau3lem  15406  limsupbnd2  15534  climrlim2  15598  climshftlem  15625  subcn2  15646  isercoll  15719  climsup  15721  serf0  15732  iseralt  15736  incexclem  15890  sqrt2irr  16305  pclem  16898  prmpwdvds  16964  vdwlem10  17050  vdwlem13  17053  ramtlecl  17060  ramub  17073  ramcl  17089  iscatd  17729  clatleglb  18574  mndind  18887  grpinveu  19041  dfgrp3lem  19104  issubg4  19212  gexdvds  19654  sylow2alem2  19688  obselocv  21847  scmatscm  22639  tgcn  23378  tgcnp  23379  lmconst  23387  cncls2  23399  cncls  23400  cnntr  23401  lmss  23424  cnt0  23472  isnrm2  23484  isreg2  23503  cmpsublem  23525  cmpsub  23526  tgcmp  23527  islly2  23610  kgencn2  23683  txdis  23758  txlm  23774  kqt0lem  23862  isr0  23863  regr1lem2  23866  cmphaushmeo  23926  cfinufil  24054  ufilen  24056  flimopn  24101  fbflim2  24103  fclsnei  24145  fclsbas  24147  fclsrest  24150  flimfnfcls  24154  fclscmp  24156  ufilcmp  24158  isfcf  24160  fcfnei  24161  cnpfcf  24167  tsmsres  24270  tsmsxp  24281  blbas  24556  prdsbl  24617  metss  24634  metcnp3  24666  bndth  25086  lebnumii  25094  iscfil3  25401  iscmet3lem1  25419  equivcfil  25427  equivcau  25428  ellimc3  26007  lhop1  26142  dvfsumrlim  26159  ftc1lem6  26169  fta1g  26296  dgrco  26401  plydivex  26427  fta1  26438  vieta1  26442  ulmshftlem  26518  ulmcaulem  26523  mtest  26533  cxpcn3lem  26878  cxploglim  27108  ftalem3  27205  dchrisumlem3  27621  pntibnd  27723  ostth2lem2  27764  n0subs  28522  grpoinveu  30812  nmcvcn  30988  blocnilem  31097  ubthlem3  31165  htthlem  31210  spansni  31850  bra11  32401  lmxrge0  34287  mrsubff1  35939  msubff1  35981  fnemeet2  36801  fnejoin2  36803  fin2so  38181  lindsenlbs  38189  poimirlem29  38223  poimirlem30  38224  ftc1cnnc  38266  incsequz2  38323  geomcau  38333  caushft  38335  sstotbnd2  38348  isbnd2  38357  totbndbnd  38363  ismtybndlem  38380  heibor  38395  atlatle  40019  cvlcvr1  40038  ltrnid  40834  ltrneq2  40847  nadd1suc  44046  climinf  46249  ralbinrald  47783  snlindsntorlem  49170