Theorem ralrimdva 3112

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  ralxfrd  5326  ralxfrd2  5330  isoselem  7192  resixpfo  8682  findcard  8908  ordtypelem2  9208  alephinit  9782  isfin2-2  10006  axpre-sup  10856  nnsub  11947  ublbneg  12602  xralrple  12868  supxrunb1  12982  expnlbnd2  13877  faclbnd4lem4  13938  hashbc  14093  cau3lem  14994  limsupbnd2  15120  climrlim2  15184  climshftlem  15211  subcn2  15232  isercoll  15307  climsup  15309  serf0  15320  iseralt  15324  incexclem  15476  sqrt2irr  15886  pclem  16467  prmpwdvds  16533  vdwlem10  16619  vdwlem13  16622  ramtlecl  16629  ramub  16642  ramcl  16658  iscatd  17299  clatleglb  18151  mndind  18381  grpinveu  18529  dfgrp3lem  18588  issubg4  18689  gexdvds  19104  sylow2alem2  19138  obselocv  20845  scmatscm  21570  tgcn  22311  tgcnp  22312  lmconst  22320  cncls2  22332  cncls  22333  cnntr  22334  lmss  22357  cnt0  22405  isnrm2  22417  isreg2  22436  cmpsublem  22458  cmpsub  22459  tgcmp  22460  islly2  22543  kgencn2  22616  txdis  22691  txlm  22707  kqt0lem  22795  isr0  22796  regr1lem2  22799  cmphaushmeo  22859  cfinufil  22987  ufilen  22989  flimopn  23034  fbflim2  23036  fclsnei  23078  fclsbas  23080  fclsrest  23083  flimfnfcls  23087  fclscmp  23089  ufilcmp  23091  isfcf  23093  fcfnei  23094  cnpfcf  23100  tsmsres  23203  tsmsxp  23214  blbas  23491  prdsbl  23553  metss  23570  metcnp3  23602  bndth  24027  lebnumii  24035  iscfil3  24342  iscmet3lem1  24360  equivcfil  24368  equivcau  24369  ellimc3  24948  lhop1  25083  dvfsumrlim  25100  ftc1lem6  25110  fta1g  25237  dgrco  25341  plydivex  25362  fta1  25373  vieta1  25377  ulmshftlem  25453  ulmcaulem  25458  mtest  25468  cxpcn3lem  25805  cxploglim  26032  ftalem3  26129  dchrisumlem3  26544  pntibnd  26646  ostth2lem2  26687  grpoinveu  28782  nmcvcn  28958  blocnilem  29067  ubthlem3  29135  htthlem  29180  spansni  29820  bra11  30371  lmxrge0  31804  mrsubff1  33376  msubff1  33418  fnemeet2  34483  fnejoin2  34485  fin2so  35691  lindsenlbs  35699  poimirlem29  35733  poimirlem30  35734  ftc1cnnc  35776  incsequz2  35834  geomcau  35844  caushft  35846  sstotbnd2  35859  isbnd2  35868  totbndbnd  35874  ismtybndlem  35891  heibor  35906  atlatle  37261  cvlcvr1  37280  ltrnid  38076  ltrneq2  38089  climinf  43037  ralbinrald  44501  snlindsntorlem  45699