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

Theorem ralrimivw 2393
 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 2391 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  ∀wral 2306 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311 This theorem is referenced by:  exse  4073  sosng  4413  dmxpm  4555  exse2  4699  funco  4940  acexmidlemph  5505  mpt2eq12  5565  xpexgALT  5760  mpt2exg  5834  rdgtfr  5961  rdgruledefgg  5962  rdgivallem  5968  frecabex  5984  frectfr  5985  omfnex  6029  oeiv  6036  oeicl  6042  uniqs  6164  genpdisj  6621  ltexprlemloc  6705  recexprlemloc  6729  cauappcvgprlemrnd  6748  cauappcvgprlemdisj  6749  caucvgprlemrnd  6771  caucvgprlemdisj  6772  caucvgprprlemrnd  6799  caucvgprprlemdisj  6800  recan  9705  climconst  9811
 Copyright terms: Public domain W3C validator