Theorem ralrimdva 3138

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 3136	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  5343  ralxfrd2  5347  isoselem  7287  resixpfo  8875  findcard  9089  ordtypelem2  9425  alephinit  10006  isfin2-2  10230  axpre-sup  11081  nnsub  12190  ublbneg  12847  xralrple  13121  supxrunb1  13235  expnlbnd2  14158  faclbnd4lem4  14220  hashbc  14377  cau3lem  15279  limsupbnd2  15407  climrlim2  15471  climshftlem  15498  subcn2  15519  isercoll  15592  climsup  15594  serf0  15605  iseralt  15609  incexclem  15760  sqrt2irr  16175  pclem  16767  prmpwdvds  16833  vdwlem10  16919  vdwlem13  16922  ramtlecl  16929  ramub  16942  ramcl  16958  iscatd  17597  clatleglb  18442  mndind  18754  grpinveu  18908  dfgrp3lem  18972  issubg4  19079  gexdvds  19517  sylow2alem2  19551  obselocv  21685  scmatscm  22456  tgcn  23195  tgcnp  23196  lmconst  23204  cncls2  23216  cncls  23217  cnntr  23218  lmss  23241  cnt0  23289  isnrm2  23301  isreg2  23320  cmpsublem  23342  cmpsub  23343  tgcmp  23344  islly2  23427  kgencn2  23500  txdis  23575  txlm  23591  kqt0lem  23679  isr0  23680  regr1lem2  23683  cmphaushmeo  23743  cfinufil  23871  ufilen  23873  flimopn  23918  fbflim2  23920  fclsnei  23962  fclsbas  23964  fclsrest  23967  flimfnfcls  23971  fclscmp  23973  ufilcmp  23975  isfcf  23977  fcfnei  23978  cnpfcf  23984  tsmsres  24087  tsmsxp  24098  blbas  24373  prdsbl  24434  metss  24451  metcnp3  24483  bndth  24903  lebnumii  24911  iscfil3  25218  iscmet3lem1  25236  equivcfil  25244  equivcau  25245  ellimc3  25824  lhop1  25960  dvfsumrlim  25979  ftc1lem6  25989  fta1g  26116  dgrco  26221  plydivex  26245  fta1  26256  vieta1  26260  ulmshftlem  26338  ulmcaulem  26343  mtest  26353  cxpcn3lem  26697  cxploglim  26928  ftalem3  27025  dchrisumlem3  27442  pntibnd  27544  ostth2lem2  27585  n0subs  28343  grpoinveu  30579  nmcvcn  30755  blocnilem  30864  ubthlem3  30932  htthlem  30977  spansni  31617  bra11  32168  lmxrge0  34102  mrsubff1  35702  msubff1  35744  fnemeet2  36555  fnejoin2  36557  fin2so  37919  lindsenlbs  37927  poimirlem29  37961  poimirlem30  37962  ftc1cnnc  38004  incsequz2  38061  geomcau  38071  caushft  38073  sstotbnd2  38086  isbnd2  38095  totbndbnd  38101  ismtybndlem  38118  heibor  38133  atlatle  39757  cvlcvr1  39776  ltrnid  40572  ltrneq2  40585  nadd1suc  43823  climinf  46040  ralbinrald  47556  snlindsntorlem  48904