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 1431 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) |
4 | 1, 3 | syl 14 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1329 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-5 1423 ax-gen 1425 |
This theorem is referenced by: albidh 1456 alrimi 1502 nfd 1503 19.21h 1536 exlimd2 1574 exlimdh 1575 eximdh 1590 nexd 1592 exbidh 1593 hbex 1615 hbnd 1633 19.12 1643 19.38 1654 ax11i 1692 equsalh 1704 nfald 1733 nfexd 1734 aev 1784 equs5or 1802 sb4or 1805 sbbidh 1817 sb6rf 1825 alrimiv 1846 eupicka 2079 2moex 2085 |
Copyright terms: Public domain | W3C validator |