Theorem ralrimdva 3191

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3145

This theorem is referenced by:  ralxfrd  5311  ralxfrd2  5315  isoselem  7096  resixpfo  8502  findcard  8759  ordtypelem2  8985  alephinit  9523  isfin2-2  9743  axpre-sup  10593  nnsub  11684  ublbneg  12336  xralrple  12601  supxrunb1  12715  expnlbnd2  13598  faclbnd4lem4  13659  hashbc  13814  cau3lem  14716  limsupbnd2  14842  climrlim2  14906  climshftlem  14933  subcn2  14953  isercoll  15026  climsup  15028  serf0  15039  iseralt  15043  incexclem  15193  sqrt2irr  15604  pclem  16177  prmpwdvds  16242  vdwlem10  16328  vdwlem13  16331  ramtlecl  16338  ramub  16351  ramcl  16367  iscatd  16946  clatleglb  17738  mndind  17994  grpinveu  18140  dfgrp3lem  18199  issubg4  18300  gexdvds  18711  sylow2alem2  18745  obselocv  20874  scmatscm  21124  tgcn  21862  tgcnp  21863  lmconst  21871  cncls2  21883  cncls  21884  cnntr  21885  lmss  21908  cnt0  21956  isnrm2  21968  isreg2  21987  cmpsublem  22009  cmpsub  22010  tgcmp  22011  islly2  22094  kgencn2  22167  txdis  22242  txlm  22258  kqt0lem  22346  isr0  22347  regr1lem2  22350  cmphaushmeo  22410  cfinufil  22538  ufilen  22540  flimopn  22585  fbflim2  22587  fclsnei  22629  fclsbas  22631  fclsrest  22634  flimfnfcls  22638  fclscmp  22640  ufilcmp  22642  isfcf  22644  fcfnei  22645  cnpfcf  22651  tsmsres  22754  tsmsxp  22765  blbas  23042  prdsbl  23103  metss  23120  metcnp3  23152  bndth  23564  lebnumii  23572  iscfil3  23878  iscmet3lem1  23896  equivcfil  23904  equivcau  23905  ellimc3  24479  lhop1  24613  dvfsumrlim  24630  ftc1lem6  24640  fta1g  24763  dgrco  24867  plydivex  24888  fta1  24899  vieta1  24903  ulmshftlem  24979  ulmcaulem  24984  mtest  24994  cxpcn3lem  25330  cxploglim  25557  ftalem3  25654  dchrisumlem3  26069  pntibnd  26171  ostth2lem2  26212  grpoinveu  28298  nmcvcn  28474  blocnilem  28583  ubthlem3  28651  htthlem  28696  spansni  29336  bra11  29887  lmxrge0  31197  mrsubff1  32763  msubff1  32805  fnemeet2  33717  fnejoin2  33719  fin2so  34881  lindsenlbs  34889  poimirlem29  34923  poimirlem30  34924  ftc1cnnc  34968  incsequz2  35026  geomcau  35036  caushft  35038  sstotbnd2  35054  isbnd2  35063  totbndbnd  35069  ismtybndlem  35086  heibor  35101  atlatle  36458  cvlcvr1  36477  ltrnid  37273  ltrneq2  37286  climinf  41894  ralbinrald  43328  snlindsntorlem  44532