Theorem ralrimdva 3106

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3069

This theorem is referenced by:  ralxfrd  5331  ralxfrd2  5335  isoselem  7212  resixpfo  8724  findcard  8946  ordtypelem2  9278  alephinit  9851  isfin2-2  10075  axpre-sup  10925  nnsub  12017  ublbneg  12673  xralrple  12939  supxrunb1  13053  expnlbnd2  13949  faclbnd4lem4  14010  hashbc  14165  cau3lem  15066  limsupbnd2  15192  climrlim2  15256  climshftlem  15283  subcn2  15304  isercoll  15379  climsup  15381  serf0  15392  iseralt  15396  incexclem  15548  sqrt2irr  15958  pclem  16539  prmpwdvds  16605  vdwlem10  16691  vdwlem13  16694  ramtlecl  16701  ramub  16714  ramcl  16730  iscatd  17382  clatleglb  18236  mndind  18466  grpinveu  18614  dfgrp3lem  18673  issubg4  18774  gexdvds  19189  sylow2alem2  19223  obselocv  20935  scmatscm  21662  tgcn  22403  tgcnp  22404  lmconst  22412  cncls2  22424  cncls  22425  cnntr  22426  lmss  22449  cnt0  22497  isnrm2  22509  isreg2  22528  cmpsublem  22550  cmpsub  22551  tgcmp  22552  islly2  22635  kgencn2  22708  txdis  22783  txlm  22799  kqt0lem  22887  isr0  22888  regr1lem2  22891  cmphaushmeo  22951  cfinufil  23079  ufilen  23081  flimopn  23126  fbflim2  23128  fclsnei  23170  fclsbas  23172  fclsrest  23175  flimfnfcls  23179  fclscmp  23181  ufilcmp  23183  isfcf  23185  fcfnei  23186  cnpfcf  23192  tsmsres  23295  tsmsxp  23306  blbas  23583  prdsbl  23647  metss  23664  metcnp3  23696  bndth  24121  lebnumii  24129  iscfil3  24437  iscmet3lem1  24455  equivcfil  24463  equivcau  24464  ellimc3  25043  lhop1  25178  dvfsumrlim  25195  ftc1lem6  25205  fta1g  25332  dgrco  25436  plydivex  25457  fta1  25468  vieta1  25472  ulmshftlem  25548  ulmcaulem  25553  mtest  25563  cxpcn3lem  25900  cxploglim  26127  ftalem3  26224  dchrisumlem3  26639  pntibnd  26741  ostth2lem2  26782  grpoinveu  28881  nmcvcn  29057  blocnilem  29166  ubthlem3  29234  htthlem  29279  spansni  29919  bra11  30470  lmxrge0  31902  mrsubff1  33476  msubff1  33518  fnemeet2  34556  fnejoin2  34558  fin2so  35764  lindsenlbs  35772  poimirlem29  35806  poimirlem30  35807  ftc1cnnc  35849  incsequz2  35907  geomcau  35917  caushft  35919  sstotbnd2  35932  isbnd2  35941  totbndbnd  35947  ismtybndlem  35964  heibor  35979  atlatle  37334  cvlcvr1  37353  ltrnid  38149  ltrneq2  38162  climinf  43147  ralbinrald  44614  snlindsntorlem  45811