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

Theorem ralrimivw 2510
 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 2508 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1481  ∀wral 2417 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422 This theorem is referenced by:  r19.27v  2563  r19.28v  2564  exse  4267  sosng  4621  dmxpm  4768  exse2  4922  funco  5172  acexmidlemph  5776  mpoeq12  5840  xpexgALT  6040  mpoexg  6118  rdgtfr  6280  rdgruledefgg  6281  rdgivallem  6287  frecabex  6304  frectfr  6306  omfnex  6354  oeiv  6361  uniqs  6496  sbthlemi5  6859  sbthlemi6  6860  updjud  6977  exmidfodomrlemim  7077  exmidaclem  7084  cc4f  7121  genpdisj  7375  ltexprlemloc  7459  recexprlemloc  7483  cauappcvgprlemrnd  7502  cauappcvgprlemdisj  7503  caucvgprlemrnd  7525  caucvgprlemdisj  7526  caucvgprprlemrnd  7553  caucvgprprlemdisj  7554  suplocexpr  7577  recan  10933  climconst  11111  sumeq2ad  11190  dvdsext  11609  neif  12369  lmconst  12444  cndis  12469
 Copyright terms: Public domain W3C validator