Theorem ralrimdva 2951

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

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 1976  ∀wral 2895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826

This theorem depends on definitions:  df-bi 195  df-an 384  df-ral 2900

This theorem is referenced by:  ralxfrd  4800  ralxfrdOLD  4801  ralxfrd2  4805  isoselem  6469  resixpfo  7809  findcard  8061  ordtypelem2  8284  alephinit  8778  isfin2-2  9001  axpre-sup  9846  nnsub  10906  ublbneg  11605  xralrple  11869  supxrunb1  11977  expnlbnd2  12812  faclbnd4lem4  12900  hashbc  13046  cau3lem  13888  limsupbnd2  14008  climrlim2  14072  climshftlem  14099  subcn2  14119  isercoll  14192  climsup  14194  serf0  14205  iseralt  14209  incexclem  14353  sqrt2irr  14763  pclem  15327  prmpwdvds  15392  vdwlem10  15478  vdwlem13  15481  ramtlecl  15488  ramub  15501  ramcl  15517  iscatd  16103  clatleglb  16895  mrcmndind  17135  grpinveu  17225  dfgrp3lem  17282  issubg4  17382  gexdvds  17768  sylow2alem2  17802  obselocv  19833  scmatscm  20080  tgcn  20808  tgcnp  20809  lmconst  20817  cncls2  20829  cncls  20830  cnntr  20831  lmss  20854  cnt0  20902  isnrm2  20914  isreg2  20933  cmpsublem  20954  cmpsub  20955  tgcmp  20956  islly2  21039  kgencn2  21112  txdis  21187  txlm  21203  kqt0lem  21291  isr0  21292  regr1lem2  21295  cmphaushmeo  21355  cfinufil  21484  ufilen  21486  flimopn  21531  fbflim2  21533  fclsnei  21575  fclsbas  21577  fclsrest  21580  flimfnfcls  21584  fclscmp  21586  ufilcmp  21588  isfcf  21590  fcfnei  21591  cnpfcf  21597  tsmsres  21699  tsmsxp  21710  blbas  21986  prdsbl  22047  metss  22064  metcnp3  22096  bndth  22496  lebnumii  22504  iscfil3  22797  iscmet3lem1  22815  equivcfil  22823  equivcau  22824  ellimc3  23366  lhop1  23498  dvfsumrlim  23515  ftc1lem6  23525  fta1g  23648  dgrco  23752  plydivex  23773  fta1  23784  vieta1  23788  ulmshftlem  23864  ulmcaulem  23869  mtest  23879  cxpcn3lem  24205  cxploglim  24421  ftalem3  24518  dchrisumlem3  24897  pntibnd  24999  ostth2lem2  25040  grpoinveu  26523  nmcvcn  26735  blocnilem  26849  ubthlem3  26918  htthlem  26964  spansni  27606  bra11  28157  lmxrge0  29132  mrsubff1  30471  msubff1  30513  fnemeet2  31338  fnejoin2  31340  fin2so  32362  lindsenlbs  32370  poimirlem29  32404  poimirlem30  32405  ftc1cnnc  32450  incsequz2  32511  geomcau  32521  caushft  32523  sstotbnd2  32539  isbnd2  32548  totbndbnd  32554  ismtybndlem  32571  heibor  32586  atlatle  33421  cvlcvr1  33440  ltrnid  34235  ltrneq2  34248  climinf  38470  ralbinrald  39645  snlindsntorlem  42048