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 2433 | 1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1433 ∀wral 2348 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-4 1440 ax-17 1459 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-ral 2353 |
This theorem is referenced by: exse 4091 sosng 4431 dmxpm 4573 exse2 4719 funco 4960 acexmidlemph 5525 mpt2eq12 5585 xpexgALT 5780 mpt2exg 5854 rdgtfr 5984 rdgruledefgg 5985 rdgivallem 5991 frecabex 6007 frectfr 6008 omfnex 6052 oeiv 6059 oeicl 6065 uniqs 6187 genpdisj 6713 ltexprlemloc 6797 recexprlemloc 6821 cauappcvgprlemrnd 6840 cauappcvgprlemdisj 6841 caucvgprlemrnd 6863 caucvgprlemdisj 6864 caucvgprprlemrnd 6891 caucvgprprlemdisj 6892 recan 9995 climconst 10129 dvdsext 10255 |
Copyright terms: Public domain | W3C validator |