Theorem ralrimdva 3164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3079

This theorem is used by:  ralxfrd  5377  ralxfrd2  5381  isoselem  7345  resixpfo  8946  findcard  9161  ordtypelem2  9494  alephinit  10101  isfin2-2  10324  axpre-sup  11181  nnsub  12307  ublbneg  12985  xralrple  13259  supxrunb1  13373  expnlbnd2  14300  faclbnd4lem4  14362  hashbc  14520  cau3lem  15444  limsupbnd2  15572  climrlim2  15636  climshftlem  15663  subcn2  15684  isercoll  15757  climsup  15759  serf0  15770  iseralt  15774  incexclem  15927  sqrt2irr  16341  pclem  16934  prmpwdvds  17000  vdwlem10  17086  vdwlem13  17089  ramtlecl  17096  ramub  17109  ramcl  17125  iscatd  17765  clatleglb  18610  mndind  18938  grpinveu  19099  dfgrp3lem  19162  issubg4  19270  gexdvds  19712  sylow2alem2  19746  obselocv  21942  lindsenlbs  22065  scmatscm  22736  tgcn  23478  tgcnp  23479  lmconst  23487  cncls2  23499  cncls  23500  cnntr  23501  lmss  23524  cnt0  23572  isnrm2  23584  isreg2  23603  cmpsublem  23625  cmpsub  23626  tgcmp  23627  islly2  23711  kgencn2  23784  txdis  23859  txlm  23875  kqt0lem  23963  isr0  23964  regr1lem2  23967  cmphaushmeo  24027  cfinufil  24155  ufilen  24157  flimopn  24202  fbflim2  24204  fclsnei  24246  fclsbas  24248  fclsrest  24251  flimfnfcls  24255  fclscmp  24257  ufilcmp  24259  isfcf  24261  fcfnei  24262  cnpfcf  24268  tsmsres  24371  tsmsxp  24382  blbas  24657  prdsbl  24718  metss  24735  metcnp3  24767  bndth  25187  lebnumii  25195  iscfil3  25502  iscmet3lem1  25520  equivcfil  25528  equivcau  25529  ellimc3  26108  lhop1  26243  dvfsumrlim  26260  ftc1lem6  26270  fta1g  26397  dgrco  26502  plydivex  26528  fta1  26539  vieta1  26543  ulmshftlem  26622  ulmcaulem  26627  mtest  26637  cxpcn3lem  26982  cxploglim  27212  ftalem3  27309  dchrisumlem3  27725  pntibnd  27827  ostth2lem2  27868  n0subs  28626  grpoinveu  30986  nmcvcn  31162  blocnilem  31271  ubthlem3  31339  htthlem  31384  spansni  32024  bra11  32575  lmxrge0  34449  mrsubff1  36080  msubff1  36122  fnemeet2  36973  fnejoin2  36975  fin2so  38348  poimirlem29  38385  poimirlem30  38386  ftc1cnnc  38428  incsequz2  38486  geomcau  38496  caushft  38498  sstotbnd2  38511  isbnd2  38520  totbndbnd  38526  ismtybndlem  38543  heibor  38558  atlatle  40180  cvlcvr1  40199  ltrnid  40995  ltrneq2  41008  nadd1suc  44220  climinf  46423  ralbinrald  47997  snlindsntorlem  49387