Theorem ralrimdva 2952

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ral 2901

This theorem is referenced by:  ralxfrd  4805  ralxfrdOLD  4806  ralxfrd2  4810  isoselem  6491  resixpfo  7832  findcard  8084  ordtypelem2  8307  alephinit  8801  isfin2-2  9024  axpre-sup  9869  nnsub  10936  ublbneg  11649  xralrple  11910  supxrunb1  12021  expnlbnd2  12857  faclbnd4lem4  12945  hashbc  13094  cau3lem  13942  limsupbnd2  14062  climrlim2  14126  climshftlem  14153  subcn2  14173  isercoll  14246  climsup  14248  serf0  14259  iseralt  14263  incexclem  14407  sqrt2irr  14817  pclem  15381  prmpwdvds  15446  vdwlem10  15532  vdwlem13  15535  ramtlecl  15542  ramub  15555  ramcl  15571  iscatd  16157  clatleglb  16949  mrcmndind  17189  grpinveu  17279  dfgrp3lem  17336  issubg4  17436  gexdvds  17822  sylow2alem2  17856  obselocv  19891  scmatscm  20138  tgcn  20866  tgcnp  20867  lmconst  20875  cncls2  20887  cncls  20888  cnntr  20889  lmss  20912  cnt0  20960  isnrm2  20972  isreg2  20991  cmpsublem  21012  cmpsub  21013  tgcmp  21014  islly2  21097  kgencn2  21170  txdis  21245  txlm  21261  kqt0lem  21349  isr0  21350  regr1lem2  21353  cmphaushmeo  21413  cfinufil  21542  ufilen  21544  flimopn  21589  fbflim2  21591  fclsnei  21633  fclsbas  21635  fclsrest  21638  flimfnfcls  21642  fclscmp  21644  ufilcmp  21646  isfcf  21648  fcfnei  21649  cnpfcf  21655  tsmsres  21757  tsmsxp  21768  blbas  22045  prdsbl  22106  metss  22123  metcnp3  22155  bndth  22565  lebnumii  22573  iscfil3  22879  iscmet3lem1  22897  equivcfil  22905  equivcau  22906  ellimc3  23449  lhop1  23581  dvfsumrlim  23598  ftc1lem6  23608  fta1g  23731  dgrco  23835  plydivex  23856  fta1  23867  vieta1  23871  ulmshftlem  23947  ulmcaulem  23952  mtest  23962  cxpcn3lem  24288  cxploglim  24504  ftalem3  24601  dchrisumlem3  24980  pntibnd  25082  ostth2lem2  25123  grpoinveu  26757  nmcvcn  26934  blocnilem  27043  ubthlem3  27112  htthlem  27158  spansni  27800  bra11  28351  lmxrge0  29326  mrsubff1  30665  msubff1  30707  fnemeet2  31532  fnejoin2  31534  fin2so  32566  lindsenlbs  32574  poimirlem29  32608  poimirlem30  32609  ftc1cnnc  32654  incsequz2  32715  geomcau  32725  caushft  32727  sstotbnd2  32743  isbnd2  32752  totbndbnd  32758  ismtybndlem  32775  heibor  32790  atlatle  33625  cvlcvr1  33644  ltrnid  34439  ltrneq2  34452  climinf  38673  ralbinrald  39848  snlindsntorlem  42053