Theorem ralrimdva 3150

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2106  ∀wral 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ral 3094

This theorem is referenced by:  ralxfrd  5120  ralxfrd2  5124  isoselem  6863  resixpfo  8232  findcard  8487  ordtypelem2  8713  alephinit  9251  isfin2-2  9476  axpre-sup  10326  nnsub  11419  ublbneg  12080  xralrple  12348  supxrunb1  12461  expnlbnd2  13314  faclbnd4lem4  13401  hashbc  13551  cau3lem  14501  limsupbnd2  14622  climrlim2  14686  climshftlem  14713  subcn2  14733  isercoll  14806  climsup  14808  serf0  14819  iseralt  14823  incexclem  14972  sqrt2irr  15382  pclem  15947  prmpwdvds  16012  vdwlem10  16098  vdwlem13  16101  ramtlecl  16108  ramub  16121  ramcl  16137  iscatd  16719  clatleglb  17512  mrcmndind  17752  grpinveu  17843  dfgrp3lem  17900  issubg4  17997  gexdvds  18383  sylow2alem2  18417  obselocv  20471  scmatscm  20724  tgcn  21464  tgcnp  21465  lmconst  21473  cncls2  21485  cncls  21486  cnntr  21487  lmss  21510  cnt0  21558  isnrm2  21570  isreg2  21589  cmpsublem  21611  cmpsub  21612  tgcmp  21613  islly2  21696  kgencn2  21769  txdis  21844  txlm  21860  kqt0lem  21948  isr0  21949  regr1lem2  21952  cmphaushmeo  22012  cfinufil  22140  ufilen  22142  flimopn  22187  fbflim2  22189  fclsnei  22231  fclsbas  22233  fclsrest  22236  flimfnfcls  22240  fclscmp  22242  ufilcmp  22244  isfcf  22246  fcfnei  22247  cnpfcf  22253  tsmsres  22355  tsmsxp  22366  blbas  22643  prdsbl  22704  metss  22721  metcnp3  22753  bndth  23165  lebnumii  23173  iscfil3  23479  iscmet3lem1  23497  equivcfil  23505  equivcau  23506  ellimc3  24080  lhop1  24214  dvfsumrlim  24231  ftc1lem6  24241  fta1g  24364  dgrco  24468  plydivex  24489  fta1  24500  vieta1  24504  ulmshftlem  24580  ulmcaulem  24585  mtest  24595  cxpcn3lem  24928  cxploglim  25156  ftalem3  25253  dchrisumlem3  25632  pntibnd  25734  ostth2lem2  25775  grpoinveu  27946  nmcvcn  28122  blocnilem  28231  ubthlem3  28300  htthlem  28346  spansni  28988  bra11  29539  lmxrge0  30596  mrsubff1  32010  msubff1  32052  fnemeet2  32950  fnejoin2  32952  fin2so  34016  lindsenlbs  34025  poimirlem29  34059  poimirlem30  34060  ftc1cnnc  34104  incsequz2  34164  geomcau  34174  caushft  34176  sstotbnd2  34192  isbnd2  34201  totbndbnd  34207  ismtybndlem  34224  heibor  34239  atlatle  35469  cvlcvr1  35488  ltrnid  36284  ltrneq2  36297  climinf  40739  ralbinrald  42156  snlindsntorlem  43267