Theorem ralrimdva 3115

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2110  ∀wral 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3071

This theorem is referenced by:  ralxfrd  5335  ralxfrd2  5339  isoselem  7206  resixpfo  8705  findcard  8926  ordtypelem2  9254  alephinit  9850  isfin2-2  10074  axpre-sup  10924  nnsub  12015  ublbneg  12670  xralrple  12936  supxrunb1  13050  expnlbnd2  13945  faclbnd4lem4  14006  hashbc  14161  cau3lem  15062  limsupbnd2  15188  climrlim2  15252  climshftlem  15279  subcn2  15300  isercoll  15375  climsup  15377  serf0  15388  iseralt  15392  incexclem  15544  sqrt2irr  15954  pclem  16535  prmpwdvds  16601  vdwlem10  16687  vdwlem13  16690  ramtlecl  16697  ramub  16710  ramcl  16726  iscatd  17378  clatleglb  18232  mndind  18462  grpinveu  18610  dfgrp3lem  18669  issubg4  18770  gexdvds  19185  sylow2alem2  19219  obselocv  20931  scmatscm  21658  tgcn  22399  tgcnp  22400  lmconst  22408  cncls2  22420  cncls  22421  cnntr  22422  lmss  22445  cnt0  22493  isnrm2  22505  isreg2  22524  cmpsublem  22546  cmpsub  22547  tgcmp  22548  islly2  22631  kgencn2  22704  txdis  22779  txlm  22795  kqt0lem  22883  isr0  22884  regr1lem2  22887  cmphaushmeo  22947  cfinufil  23075  ufilen  23077  flimopn  23122  fbflim2  23124  fclsnei  23166  fclsbas  23168  fclsrest  23171  flimfnfcls  23175  fclscmp  23177  ufilcmp  23179  isfcf  23181  fcfnei  23182  cnpfcf  23188  tsmsres  23291  tsmsxp  23302  blbas  23579  prdsbl  23643  metss  23660  metcnp3  23692  bndth  24117  lebnumii  24125  iscfil3  24433  iscmet3lem1  24451  equivcfil  24459  equivcau  24460  ellimc3  25039  lhop1  25174  dvfsumrlim  25191  ftc1lem6  25201  fta1g  25328  dgrco  25432  plydivex  25453  fta1  25464  vieta1  25468  ulmshftlem  25544  ulmcaulem  25549  mtest  25559  cxpcn3lem  25896  cxploglim  26123  ftalem3  26220  dchrisumlem3  26635  pntibnd  26737  ostth2lem2  26778  grpoinveu  28875  nmcvcn  29051  blocnilem  29160  ubthlem3  29228  htthlem  29273  spansni  29913  bra11  30464  lmxrge0  31896  mrsubff1  33470  msubff1  33512  fnemeet2  34550  fnejoin2  34552  fin2so  35758  lindsenlbs  35766  poimirlem29  35800  poimirlem30  35801  ftc1cnnc  35843  incsequz2  35901  geomcau  35911  caushft  35913  sstotbnd2  35926  isbnd2  35935  totbndbnd  35941  ismtybndlem  35958  heibor  35973  atlatle  37328  cvlcvr1  37347  ltrnid  38143  ltrneq2  38156  climinf  43116  ralbinrald  44580  snlindsntorlem  45778