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

Theorem ralrimdva 2537
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 2536 1 (𝜑 → (𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 2128  wral 2435
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 1427  ax-gen 1429  ax-4 1490  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440
This theorem is referenced by:  ralxfrd  4422  isoselem  5770  isosolem  5774  findcard  6833  nnsub  8872  supinfneg  9506  infsupneg  9507  ublbneg  9522  expnlbnd2  10543  cau3lem  11014  climshftlemg  11199  subcn2  11208  serf0  11249  sqrt2irr  12037  tgcn  12619  tgcnp  12620  lmconst  12627  cnntr  12636  lmss  12657  txdis  12688  txlm  12690  blbas  12844  metss  12905  metcnp3  12922  iswomni0  13633
  Copyright terms: Public domain W3C validator