Metamath Proof Explorer

Theorem ltstrine

Description: Trichotomy law for surreals. (Contributed by Scott Fenton, 23-Nov-2021)

Ref Expression
Assertion ltstrine 
|- ( ( A e. No /\ B e. No ) -> ( A =/= B <-> ( A

Proof

Step Hyp Ref Expression
1 ltsso 
 |-
2 sotrine 
 |-  ( (  ( A =/= B <-> ( A
3 1 2 mpan 
 |-  ( ( A e. No /\ B e. No ) -> ( A =/= B <-> ( A