Theorem ralrimdva 3162

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

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

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 1943

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

This theorem is used by:  ralxfrd  5370  ralxfrd2  5374  isoselem  7338  resixpfo  8943  findcard  9158  ordtypelem2  9491  alephinit  10131  isfin2-2  10354  axpre-sup  11211  nnsub  12337  ublbneg  13015  xralrple  13290  supxrunb1  13404  expnlbnd2  14331  faclbnd4lem4  14393  hashbc  14551  cau3lem  15475  limsupbnd2  15603  climrlim2  15667  climshftlem  15694  subcn2  15715  isercoll  15788  climsup  15790  serf0  15801  iseralt  15805  incexclem  15958  sqrt2irr  16370  pclem  16963  prmpwdvds  17029  vdwlem10  17115  vdwlem13  17118  ramtlecl  17125  ramub  17138  ramcl  17154  iscatd  17794  clatleglb  18639  mndind  18971  grpinveu  19132  dfgrp3lem  19195  issubg4  19303  gexdvds  19745  sylow2alem2  19779  obselocv  21981  lindsenlbs  22104  scmatscm  22775  tgcn  23517  tgcnp  23518  lmconst  23526  cncls2  23538  cncls  23539  cnntr  23540  lmss  23563  cnt0  23611  isnrm2  23623  isreg2  23642  cmpsublem  23664  cmpsub  23665  tgcmp  23666  islly2  23750  kgencn2  23823  txdis  23898  txlm  23914  kqt0lem  24002  isr0  24003  regr1lem2  24006  cmphaushmeo  24066  cfinufil  24194  ufilen  24196  flimopn  24241  fbflim2  24243  fclsnei  24285  fclsbas  24287  fclsrest  24290  flimfnfcls  24294  fclscmp  24296  ufilcmp  24298  isfcf  24300  fcfnei  24301  cnpfcf  24307  tsmsres  24410  tsmsxp  24421  blbas  24696  prdsbl  24757  metss  24774  metcnp3  24806  bndth  25226  lebnumii  25234  iscfil3  25541  iscmet3lem1  25559  equivcfil  25567  equivcau  25568  ellimc3  26146  lhop1  26281  dvfsumrlim  26298  ftc1lem6  26308  fta1g  26435  dgrco  26541  plydivex  26567  fta1  26578  vieta1  26584  ulmshftlem  26665  ulmcaulem  26670  mtest  26680  cxpcn3lem  27024  cxploglim  27254  ftalem3  27351  dchrisumlem3  27767  pntibnd  27869  ostth2lem2  27910  n0subs  28668  grpoinveu  31040  nmcvcn  31216  blocnilem  31325  ubthlem3  31393  htthlem  31438  spansni  32078  bra11  32629  lmxrge0  34503  mrsubff1  36194  msubff1  36236  fnemeet2  37071  fnejoin2  37073  fin2so  38444  poimirlem29  38481  poimirlem30  38482  ftc1cnnc  38524  incsequz2  38597  geomcau  38607  caushft  38609  sstotbnd2  38622  isbnd2  38631  totbndbnd  38637  ismtybndlem  38654  heibor  38669  atlatle  40291  cvlcvr1  40310  ltrnid  41106  ltrneq2  41119  nadd1suc  44331  climinf  46534  ralbinrald  48108  snlindsntorlem  49498