Metamath Proof Explorer


Theorem slttrd

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

Ref Expression
Hypotheses slttrd.1 ( 𝜑𝐴 No )
slttrd.2 ( 𝜑𝐵 No )
slttrd.3 ( 𝜑𝐶 No )
slttrd.4 ( 𝜑𝐴 <s 𝐵 )
slttrd.5 ( 𝜑𝐵 <s 𝐶 )
Assertion slttrd ( 𝜑𝐴 <s 𝐶 )

Proof

Step Hyp Ref Expression
1 slttrd.1 ( 𝜑𝐴 No )
2 slttrd.2 ( 𝜑𝐵 No )
3 slttrd.3 ( 𝜑𝐶 No )
4 slttrd.4 ( 𝜑𝐴 <s 𝐵 )
5 slttrd.5 ( 𝜑𝐵 <s 𝐶 )
6 slttr ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐴 <s 𝐵𝐵 <s 𝐶 ) → 𝐴 <s 𝐶 ) )
7 1 2 3 6 syl3anc ( 𝜑 → ( ( 𝐴 <s 𝐵𝐵 <s 𝐶 ) → 𝐴 <s 𝐶 ) )
8 4 5 7 mp2and ( 𝜑𝐴 <s 𝐶 )