Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > alrimih | Structured version Visualization version Unicode version |
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2075 and 19.21h 2121. Instance of sylg 1750. (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 1750 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-gen 1722 ax-4 1737 |
This theorem is referenced by: nexdh 1792 albidh 1793 alrimiv 1855 ax12i 1879 cbvaliw 1933 nf5dh 2026 alrimi 2082 hbnd 2147 alrimiOLD 2192 cbvalv 2273 aevALTOLD 2321 eujustALT 2473 axi5r 2594 hbralrimi 2954 bnj1093 31048 bj-abv 32901 bj-ab0 32902 mpt2bi123f 33971 axc4i-o 34183 equidq 34209 aev-o 34216 ax12f 34225 axc5c4c711 38602 hbimpg 38770 gen11nv 38842 |
Copyright terms: Public domain | W3C validator |