Metamath Proof Explorer


Theorem poleloe

Description: Express "less than or equals" for general strict orders. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion poleloe BVARIBARBA=B

Proof

Step Hyp Ref Expression
1 brun ARIBARBAIB
2 ideqg BVAIBA=B
3 2 orbi2d BVARBAIBARBA=B
4 1 3 bitrid BVARIBARBA=B