Theorem ralrimdva 3149

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∀wral 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3057

This theorem is referenced by:  ralxfrd  5402  ralxfrd2  5406  isoselem  7343  resixpfo  8946  findcard  9179  ordtypelem2  9534  alephinit  10110  isfin2-2  10334  axpre-sup  11184  nnsub  12278  ublbneg  12939  xralrple  13208  supxrunb1  13322  expnlbnd2  14220  faclbnd4lem4  14279  hashbc  14436  cau3lem  15325  limsupbnd2  15451  climrlim2  15515  climshftlem  15542  subcn2  15563  isercoll  15638  climsup  15640  serf0  15651  iseralt  15655  incexclem  15806  sqrt2irr  16217  pclem  16798  prmpwdvds  16864  vdwlem10  16950  vdwlem13  16953  ramtlecl  16960  ramub  16973  ramcl  16989  iscatd  17644  clatleglb  18501  mndind  18771  grpinveu  18922  dfgrp3lem  18985  issubg4  19091  gexdvds  19530  sylow2alem2  19564  obselocv  21649  scmatscm  22402  tgcn  23143  tgcnp  23144  lmconst  23152  cncls2  23164  cncls  23165  cnntr  23166  lmss  23189  cnt0  23237  isnrm2  23249  isreg2  23268  cmpsublem  23290  cmpsub  23291  tgcmp  23292  islly2  23375  kgencn2  23448  txdis  23523  txlm  23539  kqt0lem  23627  isr0  23628  regr1lem2  23631  cmphaushmeo  23691  cfinufil  23819  ufilen  23821  flimopn  23866  fbflim2  23868  fclsnei  23910  fclsbas  23912  fclsrest  23915  flimfnfcls  23919  fclscmp  23921  ufilcmp  23923  isfcf  23925  fcfnei  23926  cnpfcf  23932  tsmsres  24035  tsmsxp  24046  blbas  24323  prdsbl  24387  metss  24404  metcnp3  24436  bndth  24871  lebnumii  24879  iscfil3  25188  iscmet3lem1  25206  equivcfil  25214  equivcau  25215  ellimc3  25795  lhop1  25934  dvfsumrlim  25953  ftc1lem6  25963  fta1g  26091  dgrco  26197  plydivex  26219  fta1  26230  vieta1  26234  ulmshftlem  26312  ulmcaulem  26317  mtest  26327  cxpcn3lem  26669  cxploglim  26897  ftalem3  26994  dchrisumlem3  27411  pntibnd  27513  ostth2lem2  27554  grpoinveu  30316  nmcvcn  30492  blocnilem  30601  ubthlem3  30669  htthlem  30714  spansni  31354  bra11  31905  lmxrge0  33489  mrsubff1  35060  msubff1  35102  fnemeet2  35787  fnejoin2  35789  fin2so  37015  lindsenlbs  37023  poimirlem29  37057  poimirlem30  37058  ftc1cnnc  37100  incsequz2  37157  geomcau  37167  caushft  37169  sstotbnd2  37182  isbnd2  37191  totbndbnd  37197  ismtybndlem  37214  heibor  37229  atlatle  38729  cvlcvr1  38748  ltrnid  39545  ltrneq2  39558  nadd1suc  42744  climinf  44917  ralbinrald  46425  snlindsntorlem  47461