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  5405  ralxfrd2  5409  isoselem  7333  resixpfo  8926  findcard  9159  ordtypelem2  9510  alephinit  10086  isfin2-2  10310  axpre-sup  11160  nnsub  12252  ublbneg  12913  xralrple  13180  supxrunb1  13294  expnlbnd2  14193  faclbnd4lem4  14252  hashbc  14408  cau3lem  15297  limsupbnd2  15423  climrlim2  15487  climshftlem  15514  subcn2  15535  isercoll  15610  climsup  15612  serf0  15623  iseralt  15627  incexclem  15778  sqrt2irr  16188  pclem  16767  prmpwdvds  16833  vdwlem10  16919  vdwlem13  16922  ramtlecl  16929  ramub  16942  ramcl  16958  iscatd  17613  clatleglb  18467  mndind  18705  grpinveu  18855  dfgrp3lem  18917  issubg4  19019  gexdvds  19445  sylow2alem2  19479  obselocv  21267  scmatscm  21997  tgcn  22738  tgcnp  22739  lmconst  22747  cncls2  22759  cncls  22760  cnntr  22761  lmss  22784  cnt0  22832  isnrm2  22844  isreg2  22863  cmpsublem  22885  cmpsub  22886  tgcmp  22887  islly2  22970  kgencn2  23043  txdis  23118  txlm  23134  kqt0lem  23222  isr0  23223  regr1lem2  23226  cmphaushmeo  23286  cfinufil  23414  ufilen  23416  flimopn  23461  fbflim2  23463  fclsnei  23505  fclsbas  23507  fclsrest  23510  flimfnfcls  23514  fclscmp  23516  ufilcmp  23518  isfcf  23520  fcfnei  23521  cnpfcf  23527  tsmsres  23630  tsmsxp  23641  blbas  23918  prdsbl  23982  metss  23999  metcnp3  24031  bndth  24456  lebnumii  24464  iscfil3  24772  iscmet3lem1  24790  equivcfil  24798  equivcau  24799  ellimc3  25378  lhop1  25513  dvfsumrlim  25530  ftc1lem6  25540  fta1g  25667  dgrco  25771  plydivex  25792  fta1  25803  vieta1  25807  ulmshftlem  25883  ulmcaulem  25888  mtest  25898  cxpcn3lem  26235  cxploglim  26462  ftalem3  26559  dchrisumlem3  26974  pntibnd  27076  ostth2lem2  27117  grpoinveu  29750  nmcvcn  29926  blocnilem  30035  ubthlem3  30103  htthlem  30148  spansni  30788  bra11  31339  lmxrge0  32870  mrsubff1  34443  msubff1  34485  fnemeet2  35190  fnejoin2  35192  fin2so  36413  lindsenlbs  36421  poimirlem29  36455  poimirlem30  36456  ftc1cnnc  36498  incsequz2  36555  geomcau  36565  caushft  36567  sstotbnd2  36580  isbnd2  36589  totbndbnd  36595  ismtybndlem  36612  heibor  36627  atlatle  38128  cvlcvr1  38147  ltrnid  38944  ltrneq2  38957  nadd1suc  42075  climinf  44257  ralbinrald  45765  snlindsntorlem  47053