Theorem ralrimdva 3129

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  ralxfrd  5347  ralxfrd2  5351  isoselem  7278  resixpfo  8863  findcard  9077  ordtypelem2  9411  alephinit  9989  isfin2-2  10213  axpre-sup  11063  nnsub  12172  ublbneg  12834  xralrple  13107  supxrunb1  13221  expnlbnd2  14141  faclbnd4lem4  14203  hashbc  14360  cau3lem  15262  limsupbnd2  15390  climrlim2  15454  climshftlem  15481  subcn2  15502  isercoll  15575  climsup  15577  serf0  15588  iseralt  15592  incexclem  15743  sqrt2irr  16158  pclem  16750  prmpwdvds  16816  vdwlem10  16902  vdwlem13  16905  ramtlecl  16912  ramub  16925  ramcl  16941  iscatd  17579  clatleglb  18424  mndind  18702  grpinveu  18853  dfgrp3lem  18917  issubg4  19024  gexdvds  19463  sylow2alem2  19497  obselocv  21635  scmatscm  22398  tgcn  23137  tgcnp  23138  lmconst  23146  cncls2  23158  cncls  23159  cnntr  23160  lmss  23183  cnt0  23231  isnrm2  23243  isreg2  23262  cmpsublem  23284  cmpsub  23285  tgcmp  23286  islly2  23369  kgencn2  23442  txdis  23517  txlm  23533  kqt0lem  23621  isr0  23622  regr1lem2  23625  cmphaushmeo  23685  cfinufil  23813  ufilen  23815  flimopn  23860  fbflim2  23862  fclsnei  23904  fclsbas  23906  fclsrest  23909  flimfnfcls  23913  fclscmp  23915  ufilcmp  23917  isfcf  23919  fcfnei  23920  cnpfcf  23926  tsmsres  24029  tsmsxp  24040  blbas  24316  prdsbl  24377  metss  24394  metcnp3  24426  bndth  24855  lebnumii  24863  iscfil3  25171  iscmet3lem1  25189  equivcfil  25197  equivcau  25198  ellimc3  25778  lhop1  25917  dvfsumrlim  25936  ftc1lem6  25946  fta1g  26073  dgrco  26179  plydivex  26203  fta1  26214  vieta1  26218  ulmshftlem  26296  ulmcaulem  26301  mtest  26311  cxpcn3lem  26655  cxploglim  26886  ftalem3  26983  dchrisumlem3  27400  pntibnd  27502  ostth2lem2  27543  n0subs  28260  grpoinveu  30467  nmcvcn  30643  blocnilem  30752  ubthlem3  30820  htthlem  30865  spansni  31505  bra11  32056  lmxrge0  33935  mrsubff1  35507  msubff1  35549  fnemeet2  36361  fnejoin2  36363  fin2so  37607  lindsenlbs  37615  poimirlem29  37649  poimirlem30  37650  ftc1cnnc  37692  incsequz2  37749  geomcau  37759  caushft  37761  sstotbnd2  37774  isbnd2  37783  totbndbnd  37789  ismtybndlem  37806  heibor  37821  atlatle  39319  cvlcvr1  39338  ltrnid  40134  ltrneq2  40147  nadd1suc  43385  climinf  45607  ralbinrald  47126  snlindsntorlem  48475