Theorem ralrimdva 3162

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  ralxfrd  5369  ralxfrd2  5373  isoselem  7349  resixpfo  8964  findcard  9179  ordtypelem2  9513  alephinit  10174  isfin2-2  10397  axpre-sup  11254  nnsub  12382  ublbneg  13060  xralrple  13335  supxrunb1  13449  expnlbnd2  14378  faclbnd4lem4  14440  hashbc  14598  cau3lem  15522  limsupbnd2  15650  climrlim2  15714  climshftlem  15741  subcn2  15762  isercoll  15835  climsup  15837  serf0  15848  iseralt  15852  incexclem  16005  sqrt2irr  16417  pclem  17016  prmpwdvds  17082  vdwlem10  17168  vdwlem13  17171  ramtlecl  17178  ramub  17191  ramcl  17207  iscatd  17847  clatleglb  18692  mndind  19024  grpinveu  19185  dfgrp3lem  19248  issubg4  19356  gexdvds  19798  sylow2alem2  19832  obselocv  22034  lindsenlbs  22157  scmatscm  22828  tgcn  23570  tgcnp  23571  lmconst  23579  cncls2  23591  cncls  23592  cnntr  23593  lmss  23616  cnt0  23664  isnrm2  23676  isreg2  23695  cmpsublem  23717  cmpsub  23718  tgcmp  23719  islly2  23803  kgencn2  23876  txdis  23951  txlm  23967  kqt0lem  24055  isr0  24056  regr1lem2  24059  cmphaushmeo  24119  cfinufil  24247  ufilen  24249  flimopn  24294  fbflim2  24296  fclsnei  24338  fclsbas  24340  fclsrest  24343  flimfnfcls  24347  fclscmp  24349  ufilcmp  24351  isfcf  24353  fcfnei  24354  cnpfcf  24360  tsmsres  24463  tsmsxp  24474  blbas  24749  prdsbl  24810  metss  24827  metcnp3  24859  bndth  25279  lebnumii  25287  iscfil3  25594  iscmet3lem1  25612  equivcfil  25620  equivcau  25621  ellimc3  26199  lhop1  26334  dvfsumrlim  26351  ftc1lem6  26361  fta1g  26488  dgrco  26594  plydivex  26618  fta1  26629  vieta1  26635  ulmshftlem  26716  ulmcaulem  26721  mtest  26731  cxpcn3lem  27075  cxploglim  27305  ftalem3  27402  dchrisumlem3  27818  pntibnd  27920  ostth2lem2  27961  n0subs  28749  grpoinveu  31121  nmcvcn  31297  blocnilem  31406  ubthlem3  31474  htthlem  31519  spansni  32159  bra11  32710  lmxrge0  34584  mrsubff1  36279  msubff1  36321  fnemeet2  37155  fnejoin2  37157  fin2so  38531  poimirlem29  38568  poimirlem30  38569  ftc1cnnc  38611  incsequz2  38684  geomcau  38694  caushft  38696  sstotbnd2  38709  isbnd2  38718  totbndbnd  38724  ismtybndlem  38741  heibor  38756  atlatle  40378  cvlcvr1  40397  ltrnid  41193  ltrneq2  41206  nadd1suc  44394  climinf  46618  ralbinrald  48192  snlindsntorlem  49582