![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > alrimih | Structured version Visualization version GIF version |
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2201 and 19.21h 2284. Instance of sylg 1826. (Contributed by NM, 9-Jan-1993.) (Revised by BJ, 31-Mar-2021.) |
Ref | Expression |
---|---|
alrimih.1 | ⊢ (𝜑 → ∀𝑥𝜑) |
alrimih.2 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
alrimih | ⊢ (𝜑 → ∀𝑥𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alrimih.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
2 | alrimih.2 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | sylg 1826 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1798 ax-4 1812 |
This theorem is referenced by: nexdh 1869 albidh 1870 alrimiv 1931 ax12i 1971 cbvaliw 2010 nf5dh 2144 alrimi 2207 hbnd 2293 cbv3v 2332 cbv3 2396 eujustALT 2567 axi5r 2696 hbralrimi 3138 ralidmw 4466 bnj1093 33649 bj-abvALT 35420 bj-gabssd 35452 mpobi123f 36667 axc4i-o 37406 equidq 37432 aev-o 37439 ax12f 37448 axc5c4c711 42769 hbimpg 42924 gen11nv 42987 |
Copyright terms: Public domain | W3C validator |