Metamath Proof Explorer


Theorem sltletr

Description: Surreal transitive law. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion sltletr ANoBNoCNoA<sBBsCA<sC

Proof

Step Hyp Ref Expression
1 slenlt BNoCNoBsC¬C<sB
2 1 3adant1 ANoBNoCNoBsC¬C<sB
3 2 anbi2d ANoBNoCNoA<sBBsCA<sB¬C<sB
4 sltso <sOrNo
5 sotr3 <sOrNoANoBNoCNoA<sB¬C<sBA<sC
6 4 5 mpan ANoBNoCNoA<sB¬C<sBA<sC
7 3 6 sylbid ANoBNoCNoA<sBBsCA<sC