Theorem ralrimdva 3164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079

This theorem is used by:  ralxfrd  5378  ralxfrd2  5382  isoselem  7339  resixpfo  8932  findcard  9146  ordtypelem2  9479  alephinit  10086  isfin2-2  10309  axpre-sup  11160  nnsub  12286  ublbneg  12963  xralrple  13237  supxrunb1  13351  expnlbnd2  14277  faclbnd4lem4  14339  hashbc  14497  cau3lem  15413  limsupbnd2  15541  climrlim2  15605  climshftlem  15632  subcn2  15653  isercoll  15726  climsup  15728  serf0  15739  iseralt  15743  incexclem  15897  sqrt2irr  16311  pclem  16904  prmpwdvds  16970  vdwlem10  17056  vdwlem13  17059  ramtlecl  17066  ramub  17079  ramcl  17095  iscatd  17735  clatleglb  18580  mndind  18893  grpinveu  19047  dfgrp3lem  19110  issubg4  19218  gexdvds  19660  sylow2alem2  19694  obselocv  21889  scmatscm  22681  tgcn  23420  tgcnp  23421  lmconst  23429  cncls2  23441  cncls  23442  cnntr  23443  lmss  23466  cnt0  23514  isnrm2  23526  isreg2  23545  cmpsublem  23567  cmpsub  23568  tgcmp  23569  islly2  23652  kgencn2  23725  txdis  23800  txlm  23816  kqt0lem  23904  isr0  23905  regr1lem2  23908  cmphaushmeo  23968  cfinufil  24096  ufilen  24098  flimopn  24143  fbflim2  24145  fclsnei  24187  fclsbas  24189  fclsrest  24192  flimfnfcls  24196  fclscmp  24198  ufilcmp  24200  isfcf  24202  fcfnei  24203  cnpfcf  24209  tsmsres  24312  tsmsxp  24323  blbas  24598  prdsbl  24659  metss  24676  metcnp3  24708  bndth  25128  lebnumii  25136  iscfil3  25443  iscmet3lem1  25461  equivcfil  25469  equivcau  25470  ellimc3  26049  lhop1  26184  dvfsumrlim  26201  ftc1lem6  26211  fta1g  26338  dgrco  26443  plydivex  26469  fta1  26480  vieta1  26484  ulmshftlem  26563  ulmcaulem  26568  mtest  26578  cxpcn3lem  26923  cxploglim  27153  ftalem3  27250  dchrisumlem3  27666  pntibnd  27768  ostth2lem2  27809  n0subs  28567  grpoinveu  30882  nmcvcn  31058  blocnilem  31167  ubthlem3  31235  htthlem  31280  spansni  31920  bra11  32471  lmxrge0  34351  mrsubff1  36014  msubff1  36056  fnemeet2  36906  fnejoin2  36908  fin2so  38286  lindsenlbs  38294  poimirlem29  38328  poimirlem30  38329  ftc1cnnc  38371  incsequz2  38428  geomcau  38438  caushft  38440  sstotbnd2  38453  isbnd2  38462  totbndbnd  38468  ismtybndlem  38485  heibor  38500  atlatle  40122  cvlcvr1  40141  ltrnid  40937  ltrneq2  40950  nadd1suc  44147  climinf  46350  ralbinrald  47887  snlindsntorlem  49278