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

Theorem ralrimdva 2489
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 2488 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1465  wral 2393
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398
This theorem is referenced by:  ralxfrd  4353  isoselem  5689  isosolem  5693  findcard  6750  nnsub  8727  supinfneg  9358  infsupneg  9359  ublbneg  9373  expnlbnd2  10385  cau3lem  10854  climshftlemg  11039  subcn2  11048  serf0  11089  sqrt2irr  11767  tgcn  12304  tgcnp  12305  lmconst  12312  cnntr  12321  lmss  12342  txdis  12373  txlm  12375  blbas  12529  metss  12590  metcnp3  12607
  Copyright terms: Public domain W3C validator