Theorem ralrimdva 3107

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988

This theorem depends on definitions:  df-bi 197  df-an 385  df-ral 3055

This theorem is referenced by:  ralxfrd  5028  ralxfrdOLD  5029  ralxfrd2  5033  isoselem  6755  resixpfo  8114  findcard  8366  ordtypelem2  8591  alephinit  9128  isfin2-2  9353  axpre-sup  10202  nnsub  11271  ublbneg  11986  xralrple  12249  supxrunb1  12362  expnlbnd2  13209  faclbnd4lem4  13297  hashbc  13449  cau3lem  14313  limsupbnd2  14433  climrlim2  14497  climshftlem  14524  subcn2  14544  isercoll  14617  climsup  14619  serf0  14630  iseralt  14634  incexclem  14787  sqrt2irr  15198  pclem  15765  prmpwdvds  15830  vdwlem10  15916  vdwlem13  15919  ramtlecl  15926  ramub  15939  ramcl  15955  iscatd  16555  clatleglb  17347  mrcmndind  17587  grpinveu  17677  dfgrp3lem  17734  issubg4  17834  gexdvds  18219  sylow2alem2  18253  obselocv  20294  scmatscm  20541  tgcn  21278  tgcnp  21279  lmconst  21287  cncls2  21299  cncls  21300  cnntr  21301  lmss  21324  cnt0  21372  isnrm2  21384  isreg2  21403  cmpsublem  21424  cmpsub  21425  tgcmp  21426  islly2  21509  kgencn2  21582  txdis  21657  txlm  21673  kqt0lem  21761  isr0  21762  regr1lem2  21765  cmphaushmeo  21825  cfinufil  21953  ufilen  21955  flimopn  22000  fbflim2  22002  fclsnei  22044  fclsbas  22046  fclsrest  22049  flimfnfcls  22053  fclscmp  22055  ufilcmp  22057  isfcf  22059  fcfnei  22060  cnpfcf  22066  tsmsres  22168  tsmsxp  22179  blbas  22456  prdsbl  22517  metss  22534  metcnp3  22566  bndth  22978  lebnumii  22986  iscfil3  23291  iscmet3lem1  23309  equivcfil  23317  equivcau  23318  ellimc3  23862  lhop1  23996  dvfsumrlim  24013  ftc1lem6  24023  fta1g  24146  dgrco  24250  plydivex  24271  fta1  24282  vieta1  24286  ulmshftlem  24362  ulmcaulem  24367  mtest  24377  cxpcn3lem  24708  cxploglim  24924  ftalem3  25021  dchrisumlem3  25400  pntibnd  25502  ostth2lem2  25543  grpoinveu  27703  nmcvcn  27880  blocnilem  27989  ubthlem3  28058  htthlem  28104  spansni  28746  bra11  29297  lmxrge0  30328  mrsubff1  31739  msubff1  31781  fnemeet2  32689  fnejoin2  32691  fin2so  33727  lindsenlbs  33735  poimirlem29  33769  poimirlem30  33770  ftc1cnnc  33815  incsequz2  33876  geomcau  33886  caushft  33888  sstotbnd2  33904  isbnd2  33913  totbndbnd  33919  ismtybndlem  33936  heibor  33951  atlatle  35128  cvlcvr1  35147  ltrnid  35942  ltrneq2  35955  climinf  40359  ralbinrald  41723  snlindsntorlem  42787