Theorem ralrimdva 3155

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  ralxfrd  5407  ralxfrd2  5411  isoselem  7338  resixpfo  8930  findcard  9163  ordtypelem2  9514  alephinit  10090  isfin2-2  10314  axpre-sup  11164  nnsub  12256  ublbneg  12917  xralrple  13184  supxrunb1  13298  expnlbnd2  14197  faclbnd4lem4  14256  hashbc  14412  cau3lem  15301  limsupbnd2  15427  climrlim2  15491  climshftlem  15518  subcn2  15539  isercoll  15614  climsup  15616  serf0  15627  iseralt  15631  incexclem  15782  sqrt2irr  16192  pclem  16771  prmpwdvds  16837  vdwlem10  16923  vdwlem13  16926  ramtlecl  16933  ramub  16946  ramcl  16962  iscatd  17617  clatleglb  18471  mndind  18709  grpinveu  18859  dfgrp3lem  18921  issubg4  19025  gexdvds  19452  sylow2alem2  19486  obselocv  21283  scmatscm  22015  tgcn  22756  tgcnp  22757  lmconst  22765  cncls2  22777  cncls  22778  cnntr  22779  lmss  22802  cnt0  22850  isnrm2  22862  isreg2  22881  cmpsublem  22903  cmpsub  22904  tgcmp  22905  islly2  22988  kgencn2  23061  txdis  23136  txlm  23152  kqt0lem  23240  isr0  23241  regr1lem2  23244  cmphaushmeo  23304  cfinufil  23432  ufilen  23434  flimopn  23479  fbflim2  23481  fclsnei  23523  fclsbas  23525  fclsrest  23528  flimfnfcls  23532  fclscmp  23534  ufilcmp  23536  isfcf  23538  fcfnei  23539  cnpfcf  23545  tsmsres  23648  tsmsxp  23659  blbas  23936  prdsbl  24000  metss  24017  metcnp3  24049  bndth  24474  lebnumii  24482  iscfil3  24790  iscmet3lem1  24808  equivcfil  24816  equivcau  24817  ellimc3  25396  lhop1  25531  dvfsumrlim  25548  ftc1lem6  25558  fta1g  25685  dgrco  25789  plydivex  25810  fta1  25821  vieta1  25825  ulmshftlem  25901  ulmcaulem  25906  mtest  25916  cxpcn3lem  26255  cxploglim  26482  ftalem3  26579  dchrisumlem3  26994  pntibnd  27096  ostth2lem2  27137  grpoinveu  29772  nmcvcn  29948  blocnilem  30057  ubthlem3  30125  htthlem  30170  spansni  30810  bra11  31361  lmxrge0  32932  mrsubff1  34505  msubff1  34547  fnemeet2  35252  fnejoin2  35254  fin2so  36475  lindsenlbs  36483  poimirlem29  36517  poimirlem30  36518  ftc1cnnc  36560  incsequz2  36617  geomcau  36627  caushft  36629  sstotbnd2  36642  isbnd2  36651  totbndbnd  36657  ismtybndlem  36674  heibor  36689  atlatle  38190  cvlcvr1  38209  ltrnid  39006  ltrneq2  39019  nadd1suc  42142  climinf  44322  ralbinrald  45830  snlindsntorlem  47151