![]() |
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 2205 and 19.21h 2291. Instance of sylg 1824. (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 1824 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1536 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1797 ax-4 1811 |
This theorem is referenced by: nexdh 1866 albidh 1867 alrimiv 1928 ax12i 1969 cbvaliw 2013 nf5dh 2148 alrimi 2211 sbbibOLD 2285 hbnd 2300 cbv3v 2344 cbv3 2404 cbvalvOLD 2409 eujustALT 2632 axi5r 2762 hbralrimi 3147 bnj1093 32362 bj-abv 34347 bj-ab0 34348 mpobi123f 35600 axc4i-o 36194 equidq 36220 aev-o 36227 ax12f 36236 axc5c4c711 41105 hbimpg 41260 gen11nv 41323 |
Copyright terms: Public domain | W3C validator |