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 2536 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2135 ∀wral 2442 |
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 1434 ax-gen 1436 ax-4 1497 ax-17 1513 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-ral 2447 |
This theorem is referenced by: r19.27v 2591 r19.28v 2592 exse 4308 sosng 4671 dmxpm 4818 exse2 4972 funco 5222 acexmidlemph 5829 mpoeq12 5893 xpexgALT 6093 mpoexg 6171 rdgtfr 6333 rdgruledefgg 6334 rdgivallem 6340 frecabex 6357 frectfr 6359 omfnex 6408 oeiv 6415 uniqs 6550 sbthlemi5 6917 sbthlemi6 6918 updjud 7038 exmidfodomrlemim 7148 exmidaclem 7155 cc4f 7201 genpdisj 7455 ltexprlemloc 7539 recexprlemloc 7563 cauappcvgprlemrnd 7582 cauappcvgprlemdisj 7583 caucvgprlemrnd 7605 caucvgprlemdisj 7606 caucvgprprlemrnd 7633 caucvgprprlemdisj 7634 suplocexpr 7657 recan 11037 climconst 11217 sumeq2ad 11296 dvdsext 11778 zsupssdc 11872 pc11 12241 neif 12688 lmconst 12763 cndis 12788 |
Copyright terms: Public domain | W3C validator |