Theorem ralrimdva 3138

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

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

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 3053

This theorem is referenced by:  ralxfrd  5347  ralxfrd2  5351  isoselem  7291  resixpfo  8879  findcard  9093  ordtypelem2  9429  alephinit  10012  isfin2-2  10236  axpre-sup  11087  nnsub  12216  ublbneg  12878  xralrple  13152  supxrunb1  13266  expnlbnd2  14191  faclbnd4lem4  14253  hashbc  14410  cau3lem  15312  limsupbnd2  15440  climrlim2  15504  climshftlem  15531  subcn2  15552  isercoll  15625  climsup  15627  serf0  15638  iseralt  15642  incexclem  15796  sqrt2irr  16211  pclem  16804  prmpwdvds  16870  vdwlem10  16956  vdwlem13  16959  ramtlecl  16966  ramub  16979  ramcl  16995  iscatd  17634  clatleglb  18479  mndind  18791  grpinveu  18945  dfgrp3lem  19009  issubg4  19116  gexdvds  19554  sylow2alem2  19588  obselocv  21722  scmatscm  22492  tgcn  23231  tgcnp  23232  lmconst  23240  cncls2  23252  cncls  23253  cnntr  23254  lmss  23277  cnt0  23325  isnrm2  23337  isreg2  23356  cmpsublem  23378  cmpsub  23379  tgcmp  23380  islly2  23463  kgencn2  23536  txdis  23611  txlm  23627  kqt0lem  23715  isr0  23716  regr1lem2  23719  cmphaushmeo  23779  cfinufil  23907  ufilen  23909  flimopn  23954  fbflim2  23956  fclsnei  23998  fclsbas  24000  fclsrest  24003  flimfnfcls  24007  fclscmp  24009  ufilcmp  24011  isfcf  24013  fcfnei  24014  cnpfcf  24020  tsmsres  24123  tsmsxp  24134  blbas  24409  prdsbl  24470  metss  24487  metcnp3  24519  bndth  24939  lebnumii  24947  iscfil3  25254  iscmet3lem1  25272  equivcfil  25280  equivcau  25281  ellimc3  25860  lhop1  25995  dvfsumrlim  26012  ftc1lem6  26022  fta1g  26149  dgrco  26254  plydivex  26278  fta1  26289  vieta1  26293  ulmshftlem  26371  ulmcaulem  26376  mtest  26386  cxpcn3lem  26728  cxploglim  26959  ftalem3  27056  dchrisumlem3  27472  pntibnd  27574  ostth2lem2  27615  n0subs  28373  grpoinveu  30609  nmcvcn  30785  blocnilem  30894  ubthlem3  30962  htthlem  31007  spansni  31647  bra11  32198  lmxrge0  34116  mrsubff1  35716  msubff1  35758  fnemeet2  36569  fnejoin2  36571  fin2so  37948  lindsenlbs  37956  poimirlem29  37990  poimirlem30  37991  ftc1cnnc  38033  incsequz2  38090  geomcau  38100  caushft  38102  sstotbnd2  38115  isbnd2  38124  totbndbnd  38130  ismtybndlem  38147  heibor  38162  atlatle  39786  cvlcvr1  39805  ltrnid  40601  ltrneq2  40614  nadd1suc  43844  climinf  46060  ralbinrald  47588  snlindsntorlem  48964