Theorem ralrimdva 3152

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∀wral 3059

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  ralxfrd  5405  ralxfrd2  5409  isoselem  7340  resixpfo  8932  findcard  9165  ordtypelem2  9516  alephinit  10092  isfin2-2  10316  axpre-sup  11166  nnsub  12260  ublbneg  12921  xralrple  13188  supxrunb1  13302  expnlbnd2  14201  faclbnd4lem4  14260  hashbc  14416  cau3lem  15305  limsupbnd2  15431  climrlim2  15495  climshftlem  15522  subcn2  15543  isercoll  15618  climsup  15620  serf0  15631  iseralt  15635  incexclem  15786  sqrt2irr  16196  pclem  16775  prmpwdvds  16841  vdwlem10  16927  vdwlem13  16930  ramtlecl  16937  ramub  16950  ramcl  16966  iscatd  17621  clatleglb  18475  mndind  18745  grpinveu  18895  dfgrp3lem  18957  issubg4  19061  gexdvds  19493  sylow2alem2  19527  obselocv  21502  scmatscm  22235  tgcn  22976  tgcnp  22977  lmconst  22985  cncls2  22997  cncls  22998  cnntr  22999  lmss  23022  cnt0  23070  isnrm2  23082  isreg2  23101  cmpsublem  23123  cmpsub  23124  tgcmp  23125  islly2  23208  kgencn2  23281  txdis  23356  txlm  23372  kqt0lem  23460  isr0  23461  regr1lem2  23464  cmphaushmeo  23524  cfinufil  23652  ufilen  23654  flimopn  23699  fbflim2  23701  fclsnei  23743  fclsbas  23745  fclsrest  23748  flimfnfcls  23752  fclscmp  23754  ufilcmp  23756  isfcf  23758  fcfnei  23759  cnpfcf  23765  tsmsres  23868  tsmsxp  23879  blbas  24156  prdsbl  24220  metss  24237  metcnp3  24269  bndth  24704  lebnumii  24712  iscfil3  25021  iscmet3lem1  25039  equivcfil  25047  equivcau  25048  ellimc3  25628  lhop1  25766  dvfsumrlim  25783  ftc1lem6  25793  fta1g  25920  dgrco  26025  plydivex  26046  fta1  26057  vieta1  26061  ulmshftlem  26137  ulmcaulem  26142  mtest  26152  cxpcn3lem  26491  cxploglim  26718  ftalem3  26815  dchrisumlem3  27230  pntibnd  27332  ostth2lem2  27373  grpoinveu  30039  nmcvcn  30215  blocnilem  30324  ubthlem3  30392  htthlem  30437  spansni  31077  bra11  31628  lmxrge0  33230  mrsubff1  34803  msubff1  34845  fnemeet2  35555  fnejoin2  35557  fin2so  36778  lindsenlbs  36786  poimirlem29  36820  poimirlem30  36821  ftc1cnnc  36863  incsequz2  36920  geomcau  36930  caushft  36932  sstotbnd2  36945  isbnd2  36954  totbndbnd  36960  ismtybndlem  36977  heibor  36992  atlatle  38493  cvlcvr1  38512  ltrnid  39309  ltrneq2  39322  nadd1suc  42444  climinf  44620  ralbinrald  46128  snlindsntorlem  47238