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 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 |