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

Theorem ralrimdva 2510
 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 2509 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1480  ∀wral 2414 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 1423  ax-gen 1425  ax-4 1487  ax-17 1506 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419 This theorem is referenced by:  ralxfrd  4378  isoselem  5714  isosolem  5718  findcard  6775  nnsub  8752  supinfneg  9383  infsupneg  9384  ublbneg  9398  expnlbnd2  10410  cau3lem  10879  climshftlemg  11064  subcn2  11073  serf0  11114  sqrt2irr  11829  tgcn  12366  tgcnp  12367  lmconst  12374  cnntr  12383  lmss  12404  txdis  12435  txlm  12437  blbas  12591  metss  12652  metcnp3  12669
 Copyright terms: Public domain W3C validator