Theorem ralrimdva 3135

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3051

This theorem is referenced by:  ralxfrd  5352  ralxfrd2  5356  isoselem  7287  resixpfo  8876  findcard  9090  ordtypelem2  9426  alephinit  10007  isfin2-2  10231  axpre-sup  11082  nnsub  12191  ublbneg  12848  xralrple  13122  supxrunb1  13236  expnlbnd2  14159  faclbnd4lem4  14221  hashbc  14378  cau3lem  15280  limsupbnd2  15408  climrlim2  15472  climshftlem  15499  subcn2  15520  isercoll  15593  climsup  15595  serf0  15606  iseralt  15610  incexclem  15761  sqrt2irr  16176  pclem  16768  prmpwdvds  16834  vdwlem10  16920  vdwlem13  16923  ramtlecl  16930  ramub  16943  ramcl  16959  iscatd  17598  clatleglb  18443  mndind  18755  grpinveu  18906  dfgrp3lem  18970  issubg4  19077  gexdvds  19515  sylow2alem2  19549  obselocv  21685  scmatscm  22459  tgcn  23198  tgcnp  23199  lmconst  23207  cncls2  23219  cncls  23220  cnntr  23221  lmss  23244  cnt0  23292  isnrm2  23304  isreg2  23323  cmpsublem  23345  cmpsub  23346  tgcmp  23347  islly2  23430  kgencn2  23503  txdis  23578  txlm  23594  kqt0lem  23682  isr0  23683  regr1lem2  23686  cmphaushmeo  23746  cfinufil  23874  ufilen  23876  flimopn  23921  fbflim2  23923  fclsnei  23965  fclsbas  23967  fclsrest  23970  flimfnfcls  23974  fclscmp  23976  ufilcmp  23978  isfcf  23980  fcfnei  23981  cnpfcf  23987  tsmsres  24090  tsmsxp  24101  blbas  24376  prdsbl  24437  metss  24454  metcnp3  24486  bndth  24915  lebnumii  24923  iscfil3  25231  iscmet3lem1  25249  equivcfil  25257  equivcau  25258  ellimc3  25838  lhop1  25977  dvfsumrlim  25996  ftc1lem6  26006  fta1g  26133  dgrco  26239  plydivex  26263  fta1  26274  vieta1  26278  ulmshftlem  26356  ulmcaulem  26361  mtest  26371  cxpcn3lem  26715  cxploglim  26946  ftalem3  27043  dchrisumlem3  27460  pntibnd  27562  ostth2lem2  27603  n0subs  28340  grpoinveu  30575  nmcvcn  30751  blocnilem  30860  ubthlem3  30928  htthlem  30973  spansni  31613  bra11  32164  lmxrge0  34088  mrsubff1  35687  msubff1  35729  fnemeet2  36540  fnejoin2  36542  fin2so  37777  lindsenlbs  37785  poimirlem29  37819  poimirlem30  37820  ftc1cnnc  37862  incsequz2  37919  geomcau  37929  caushft  37931  sstotbnd2  37944  isbnd2  37953  totbndbnd  37959  ismtybndlem  37976  heibor  37991  atlatle  39615  cvlcvr1  39634  ltrnid  40430  ltrneq2  40443  nadd1suc  43671  climinf  45889  ralbinrald  47405  snlindsntorlem  48753