ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimdva GIF version

Theorem ralrimdva 2550
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Feb-2008.)
Hypothesis
Ref Expression
ralrimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralrimdva (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜓,𝑥
Allowed substitution hints:   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimdva
StepHypRef Expression
1 ralrimdva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 114 . . 3 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32com23 78 . 2 (𝜑 → (𝜓 → (𝑥𝐴𝜒)))
43ralrimdv 2549 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 2141  wral 2448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453
This theorem is referenced by:  ralxfrd  4447  isoselem  5799  isosolem  5803  findcard  6866  nnsub  8917  supinfneg  9554  infsupneg  9555  ublbneg  9572  expnlbnd2  10601  cau3lem  11078  climshftlemg  11265  subcn2  11274  serf0  11315  sqrt2irr  12116  pclemub  12241  prmpwdvds  12307  grpinveu  12741  tgcn  13002  tgcnp  13003  lmconst  13010  cnntr  13019  lmss  13040  txdis  13071  txlm  13073  blbas  13227  metss  13288  metcnp3  13305  iswomni0  14083
  Copyright terms: Public domain W3C validator