Theorem ralrimdva 3160

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  ralxfrd  5426  ralxfrd2  5430  isoselem  7377  resixpfo  8994  findcard  9229  ordtypelem2  9588  alephinit  10164  isfin2-2  10388  axpre-sup  11238  nnsub  12337  ublbneg  12998  xralrple  13267  supxrunb1  13381  expnlbnd2  14283  faclbnd4lem4  14345  hashbc  14502  cau3lem  15403  limsupbnd2  15529  climrlim2  15593  climshftlem  15620  subcn2  15641  isercoll  15716  climsup  15718  serf0  15729  iseralt  15733  incexclem  15884  sqrt2irr  16297  pclem  16885  prmpwdvds  16951  vdwlem10  17037  vdwlem13  17040  ramtlecl  17047  ramub  17060  ramcl  17076  iscatd  17731  clatleglb  18588  mndind  18863  grpinveu  19014  dfgrp3lem  19078  issubg4  19185  gexdvds  19626  sylow2alem2  19660  obselocv  21771  scmatscm  22540  tgcn  23281  tgcnp  23282  lmconst  23290  cncls2  23302  cncls  23303  cnntr  23304  lmss  23327  cnt0  23375  isnrm2  23387  isreg2  23406  cmpsublem  23428  cmpsub  23429  tgcmp  23430  islly2  23513  kgencn2  23586  txdis  23661  txlm  23677  kqt0lem  23765  isr0  23766  regr1lem2  23769  cmphaushmeo  23829  cfinufil  23957  ufilen  23959  flimopn  24004  fbflim2  24006  fclsnei  24048  fclsbas  24050  fclsrest  24053  flimfnfcls  24057  fclscmp  24059  ufilcmp  24061  isfcf  24063  fcfnei  24064  cnpfcf  24070  tsmsres  24173  tsmsxp  24184  blbas  24461  prdsbl  24525  metss  24542  metcnp3  24574  bndth  25009  lebnumii  25017  iscfil3  25326  iscmet3lem1  25344  equivcfil  25352  equivcau  25353  ellimc3  25934  lhop1  26073  dvfsumrlim  26092  ftc1lem6  26102  fta1g  26229  dgrco  26335  plydivex  26357  fta1  26368  vieta1  26372  ulmshftlem  26450  ulmcaulem  26455  mtest  26465  cxpcn3lem  26808  cxploglim  27039  ftalem3  27136  dchrisumlem3  27553  pntibnd  27655  ostth2lem2  27696  n0subs  28378  grpoinveu  30551  nmcvcn  30727  blocnilem  30836  ubthlem3  30904  htthlem  30949  spansni  31589  bra11  32140  lmxrge0  33898  mrsubff1  35482  msubff1  35524  fnemeet2  36333  fnejoin2  36335  fin2so  37567  lindsenlbs  37575  poimirlem29  37609  poimirlem30  37610  ftc1cnnc  37652  incsequz2  37709  geomcau  37719  caushft  37721  sstotbnd2  37734  isbnd2  37743  totbndbnd  37749  ismtybndlem  37766  heibor  37781  atlatle  39276  cvlcvr1  39295  ltrnid  40092  ltrneq2  40105  nadd1suc  43354  climinf  45527  ralbinrald  47037  snlindsntorlem  48199