![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > alrimih | GIF version |
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Ref | Expression |
---|---|
alrimih.1 | ⊢ (𝜑 → ∀𝑥𝜑) |
alrimih.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimih | ⊢ (𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimih.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alrimih.2 | . . 3 ⊢ (𝜑 → 𝜓) | |
3 | 2 | alimi 1466 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
4 | 1, 3 | syl 14 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1458 ax-gen 1460 |
This theorem is referenced by: albidh 1491 alrimi 1533 nfd 1534 19.21h 1568 exlimd2 1606 exlimdh 1607 eximdh 1622 nexd 1624 exbidh 1625 hbex 1647 hbnd 1666 19.12 1676 19.38 1687 ax11i 1725 equsalh 1737 nfald 1771 nfexd 1772 aev 1823 equs5or 1841 sb4or 1844 sbbidh 1856 sb6rf 1864 alrimiv 1885 eupicka 2118 2moex 2124 |
Copyright terms: Public domain | W3C validator |