![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralrimivw | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
ralrimivw.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
ralrimivw | ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralrimivw.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | 1 | a1d 22 | . 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) |
3 | 2 | ralrimiv 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 |