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

Theorem ralrimivw 2410
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
ralrimivw.1 (𝜑𝜓)
Assertion
Ref Expression
ralrimivw (𝜑 → ∀𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3 (𝜑𝜓)
21a1d 22 . 2 (𝜑 → (𝑥𝐴𝜓))
32ralrimiv 2408 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328
This theorem is referenced by:  exse  4101  sosng  4441  dmxpm  4583  exse2  4727  funco  4968  acexmidlemph  5533  mpt2eq12  5593  xpexgALT  5788  mpt2exg  5862  rdgtfr  5992  rdgruledefgg  5993  rdgivallem  5999  frecabex  6015  frectfr  6016  omfnex  6060  oeiv  6067  oeicl  6073  uniqs  6195  genpdisj  6679  ltexprlemloc  6763  recexprlemloc  6787  cauappcvgprlemrnd  6806  cauappcvgprlemdisj  6807  caucvgprlemrnd  6829  caucvgprlemdisj  6830  caucvgprprlemrnd  6857  caucvgprprlemdisj  6858  recan  9936  climconst  10042  dvdsext  10167
  Copyright terms: Public domain W3C validator