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 2209 and 19.21h 2291. Instance of sylg 1829. (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 1829 | 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 1802 ax-4 1816 |
This theorem is referenced by: nexdh 1872 albidh 1873 alrimiv 1934 ax12i 1974 cbvaliw 2018 nf5dh 2151 alrimi 2215 hbnd 2300 cbv3v 2337 cbv3 2397 eujustALT 2573 axi5r 2702 hbralrimi 3094 ralidmw 4394 bnj1093 32531 bj-abvALT 34736 bj-gabssd 34767 mpobi123f 35963 axc4i-o 36555 equidq 36581 aev-o 36588 ax12f 36597 axc5c4c711 41577 hbimpg 41732 gen11nv 41795 |
Copyright terms: Public domain | W3C validator |