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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3079

This theorem is referenced by:  ralxfrd  5367  ralxfrd2  5371  isoselem  7327  resixpfo  8920  findcard  9134  ordtypelem2  9469  alephinit  10053  isfin2-2  10278  axpre-sup  11129  nnsub  12259  ublbneg  12936  xralrple  13210  supxrunb1  13324  expnlbnd2  14249  faclbnd4lem4  14311  hashbc  14468  cau3lem  15384  limsupbnd2  15512  climrlim2  15576  climshftlem  15603  subcn2  15624  isercoll  15697  climsup  15699  serf0  15710  iseralt  15714  incexclem  15868  sqrt2irr  16283  pclem  16876  prmpwdvds  16942  vdwlem10  17028  vdwlem13  17031  ramtlecl  17038  ramub  17051  ramcl  17067  iscatd  17707  clatleglb  18552  mndind  18864  grpinveu  19018  dfgrp3lem  19082  issubg4  19189  gexdvds  19626  sylow2alem2  19660  obselocv  21782  scmatscm  22575  tgcn  23314  tgcnp  23315  lmconst  23323  cncls2  23335  cncls  23336  cnntr  23337  lmss  23360  cnt0  23408  isnrm2  23420  isreg2  23439  cmpsublem  23461  cmpsub  23462  tgcmp  23463  islly2  23546  kgencn2  23619  txdis  23694  txlm  23710  kqt0lem  23798  isr0  23799  regr1lem2  23802  cmphaushmeo  23862  cfinufil  23990  ufilen  23992  flimopn  24037  fbflim2  24039  fclsnei  24081  fclsbas  24083  fclsrest  24086  flimfnfcls  24090  fclscmp  24092  ufilcmp  24094  isfcf  24096  fcfnei  24097  cnpfcf  24103  tsmsres  24206  tsmsxp  24217  blbas  24492  prdsbl  24553  metss  24570  metcnp3  24602  bndth  25022  lebnumii  25030  iscfil3  25337  iscmet3lem1  25355  equivcfil  25363  equivcau  25364  ellimc3  25943  lhop1  26078  dvfsumrlim  26095  ftc1lem6  26105  fta1g  26232  dgrco  26337  plydivex  26363  fta1  26374  vieta1  26378  ulmshftlem  26454  ulmcaulem  26459  mtest  26469  cxpcn3lem  26814  cxploglim  27044  ftalem3  27141  dchrisumlem3  27557  pntibnd  27659  ostth2lem2  27700  n0subs  28458  grpoinveu  30724  nmcvcn  30900  blocnilem  31009  ubthlem3  31077  htthlem  31122  spansni  31762  bra11  32313  lmxrge0  34251  mrsubff1  35869  msubff1  35911  fnemeet2  36732  fnejoin2  36734  fin2so  38111  lindsenlbs  38119  poimirlem29  38153  poimirlem30  38154  ftc1cnnc  38196  incsequz2  38253  geomcau  38263  caushft  38265  sstotbnd2  38278  isbnd2  38287  totbndbnd  38293  ismtybndlem  38310  heibor  38325  atlatle  39949  cvlcvr1  39968  ltrnid  40764  ltrneq2  40777  nadd1suc  43974  climinf  46187  ralbinrald  47721  snlindsntorlem  49097