Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > alimdv | GIF version |
Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
alimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
alimdv | ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-17 1491 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alimdv.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | alimdh 1428 | 1 ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1408 ax-gen 1410 ax-17 1491 |
This theorem is referenced by: 2alimdv 1837 moim 2041 ralimdv2 2479 sstr2 3074 reuss2 3326 ssuni 3728 disjss2 3879 disjss1 3882 disjiun 3894 exmidsssnc 4096 soss 4206 alxfr 4352 ssrel 4597 ssrel2 4599 ssrelrel 4609 iotaval 5069 omnimkv 6998 |
Copyright terms: Public domain | W3C validator |