Theorem ralrimdva 3137

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053

This theorem is referenced by:  ralxfrd  5354  ralxfrd2  5358  isoselem  7289  resixpfo  8878  findcard  9092  ordtypelem2  9428  alephinit  10009  isfin2-2  10233  axpre-sup  11084  nnsub  12193  ublbneg  12850  xralrple  13124  supxrunb1  13238  expnlbnd2  14161  faclbnd4lem4  14223  hashbc  14380  cau3lem  15282  limsupbnd2  15410  climrlim2  15474  climshftlem  15501  subcn2  15522  isercoll  15595  climsup  15597  serf0  15608  iseralt  15612  incexclem  15763  sqrt2irr  16178  pclem  16770  prmpwdvds  16836  vdwlem10  16922  vdwlem13  16925  ramtlecl  16932  ramub  16945  ramcl  16961  iscatd  17600  clatleglb  18445  mndind  18757  grpinveu  18908  dfgrp3lem  18972  issubg4  19079  gexdvds  19517  sylow2alem2  19551  obselocv  21687  scmatscm  22461  tgcn  23200  tgcnp  23201  lmconst  23209  cncls2  23221  cncls  23222  cnntr  23223  lmss  23246  cnt0  23294  isnrm2  23306  isreg2  23325  cmpsublem  23347  cmpsub  23348  tgcmp  23349  islly2  23432  kgencn2  23505  txdis  23580  txlm  23596  kqt0lem  23684  isr0  23685  regr1lem2  23688  cmphaushmeo  23748  cfinufil  23876  ufilen  23878  flimopn  23923  fbflim2  23925  fclsnei  23967  fclsbas  23969  fclsrest  23972  flimfnfcls  23976  fclscmp  23978  ufilcmp  23980  isfcf  23982  fcfnei  23983  cnpfcf  23989  tsmsres  24092  tsmsxp  24103  blbas  24378  prdsbl  24439  metss  24456  metcnp3  24488  bndth  24917  lebnumii  24925  iscfil3  25233  iscmet3lem1  25251  equivcfil  25259  equivcau  25260  ellimc3  25840  lhop1  25979  dvfsumrlim  25998  ftc1lem6  26008  fta1g  26135  dgrco  26241  plydivex  26265  fta1  26276  vieta1  26280  ulmshftlem  26358  ulmcaulem  26363  mtest  26373  cxpcn3lem  26717  cxploglim  26948  ftalem3  27045  dchrisumlem3  27462  pntibnd  27564  ostth2lem2  27605  n0subs  28363  grpoinveu  30598  nmcvcn  30774  blocnilem  30883  ubthlem3  30951  htthlem  30996  spansni  31636  bra11  32187  lmxrge0  34111  mrsubff1  35710  msubff1  35752  fnemeet2  36563  fnejoin2  36565  fin2so  37810  lindsenlbs  37818  poimirlem29  37852  poimirlem30  37853  ftc1cnnc  37895  incsequz2  37952  geomcau  37962  caushft  37964  sstotbnd2  37977  isbnd2  37986  totbndbnd  37992  ismtybndlem  38009  heibor  38024  atlatle  39648  cvlcvr1  39667  ltrnid  40463  ltrneq2  40476  nadd1suc  43701  climinf  45919  ralbinrald  47435  snlindsntorlem  48783