![]() |
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 1414 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
4 | 1, 3 | syl 14 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1312 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-5 1406 ax-gen 1408 |
This theorem is referenced by: albidh 1439 alrimi 1485 nfd 1486 19.21h 1519 exlimd2 1557 exlimdh 1558 eximdh 1573 nexd 1575 exbidh 1576 hbex 1598 hbnd 1616 19.12 1626 19.38 1637 ax11i 1675 equsalh 1687 nfald 1716 nfexd 1717 aev 1766 equs5or 1784 sb4or 1787 sbbidh 1799 sb6rf 1807 alrimiv 1828 eupicka 2055 2moex 2061 |
Copyright terms: Public domain | W3C validator |