Metamath Proof Explorer


Theorem ssctOLD

Description: Obsolete version of ssct as of 7-Dec-2024. (Contributed by Thierry Arnoux, 31-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssctOLD A B B ω A ω

Proof

Step Hyp Ref Expression
1 ctex B ω B V
2 ssdomg B V A B A B
3 1 2 syl B ω A B A B
4 3 impcom A B B ω A B
5 domtr A B B ω A ω
6 4 5 sylancom A B B ω A ω