Theorem ralrimdva 3166

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  ralxfrd  5374  ralxfrd2  5378  isoselem  7369  resixpfo  8989  findcard  9204  ordtypelem2  9537  alephinit  10198  isfin2-2  10421  axpre-sup  11278  nnsub  12406  ublbneg  13084  xralrple  13359  supxrunb1  13473  expnlbnd2  14402  faclbnd4lem4  14464  hashbc  14622  cau3lem  15548  limsupbnd2  15676  climrlim2  15740  climshftlem  15767  subcn2  15788  isercoll  15861  climsup  15863  serf0  15874  iseralt  15878  incexclem  16031  sqrt2irr  16443  pclem  17042  prmpwdvds  17108  vdwlem10  17194  vdwlem13  17197  ramtlecl  17204  ramub  17217  ramcl  17233  iscatd  17873  clatleglb  18718  mndind  19050  grpinveu  19211  dfgrp3lem  19274  issubg4  19382  gexdvds  19825  sylow2alem2  19859  obselocv  22061  lindsenlbs  22184  scmatscm  22855  tgcn  23597  tgcnp  23598  lmconst  23606  cncls2  23618  cncls  23619  cnntr  23620  lmss  23643  cnt0  23691  isnrm2  23703  isreg2  23722  cmpsublem  23744  cmpsub  23745  tgcmp  23746  islly2  23830  kgencn2  23903  txdis  23978  txlm  23994  kqt0lem  24082  isr0  24083  regr1lem2  24086  cmphaushmeo  24146  cfinufil  24274  ufilen  24276  flimopn  24321  fbflim2  24323  fclsnei  24365  fclsbas  24367  fclsrest  24370  flimfnfcls  24374  fclscmp  24376  ufilcmp  24378  isfcf  24380  fcfnei  24381  cnpfcf  24387  tsmsres  24490  tsmsxp  24501  blbas  24776  prdsbl  24837  metss  24854  metcnp3  24886  bndth  25306  lebnumii  25314  iscfil3  25621  iscmet3lem1  25639  equivcfil  25647  equivcau  25648  ellimc3  26226  lhop1  26361  dvfsumrlim  26378  ftc1lem6  26388  fta1g  26515  dgrco  26621  plydivex  26645  fta1  26656  vieta1  26662  ulmshftlem  26743  ulmcaulem  26748  mtest  26758  cxpcn3lem  27102  cxploglim  27332  ftalem3  27429  dchrisumlem3  27845  pntibnd  27947  ostth2lem2  27988  n0subs  28776  grpoinveu  31148  nmcvcn  31324  blocnilem  31433  ubthlem3  31501  htthlem  31546  spansni  32186  bra11  32737  lmxrge0  34651  mrsubff1  36445  msubff1  36487  fnemeet2  37332  fnejoin2  37334  fin2so  38721  poimirlem29  38758  poimirlem30  38759  ftc1cnnc  38801  incsequz2  38874  geomcau  38884  caushft  38886  sstotbnd2  38899  isbnd2  38908  totbndbnd  38914  ismtybndlem  38931  heibor  38946  atlatle  40568  cvlcvr1  40587  ltrnid  41383  ltrneq2  41396  nadd1suc  44584  climinf  46821  ralbinrald  48396  snlindsntorlem  49785