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

Theorem ralrimivw 2478
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 2476 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1461  wral 2388
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-17 1487
This theorem depends on definitions:  df-bi 116  df-nf 1418  df-ral 2393
This theorem is referenced by:  r19.27v  2531  r19.28v  2532  exse  4216  sosng  4570  dmxpm  4717  exse2  4869  funco  5119  acexmidlemph  5719  mpoeq12  5783  xpexgALT  5983  mpoexg  6061  rdgtfr  6223  rdgruledefgg  6224  rdgivallem  6230  frecabex  6247  frectfr  6249  omfnex  6297  oeiv  6304  uniqs  6439  sbthlemi5  6799  sbthlemi6  6800  updjud  6917  exmidfodomrlemim  7002  exmidaclem  7009  genpdisj  7273  ltexprlemloc  7357  recexprlemloc  7381  cauappcvgprlemrnd  7400  cauappcvgprlemdisj  7401  caucvgprlemrnd  7423  caucvgprlemdisj  7424  caucvgprprlemrnd  7451  caucvgprprlemdisj  7452  recan  10767  climconst  10945  sumeq2ad  11024  dvdsext  11395  neif  12147  lmconst  12221  cndis  12246
  Copyright terms: Public domain W3C validator