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 2203 and 19.21h 2291. Instance of sylg 1819. (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 1819 | 1 ⊢ (𝜑 → ∀𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1792 ax-4 1806 |
This theorem is referenced by: nexdh 1862 albidh 1863 alrimiv 1924 ax12i 1965 cbvaliw 2009 nf5dh 2147 alrimi 2209 sbbibOLD 2285 hbnd 2300 cbv3v 2351 cbv3 2411 cbvalvOLD 2416 eujustALT 2653 axi5r 2783 hbralrimi 3180 bnj1093 32247 bj-abv 34218 bj-ab0 34219 mpobi123f 35434 axc4i-o 36028 equidq 36054 aev-o 36061 ax12f 36070 axc5c4c711 40726 hbimpg 40881 gen11nv 40944 |
Copyright terms: Public domain | W3C validator |