Metamath Proof Explorer

Theorem socnv

Description: The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018)

Ref Expression
Assertion socnv 
|- ( R Or A -> `' R Or A )

Proof

Step Hyp Ref Expression
1 cnvso 
 |-  ( R Or A <-> `' R Or A )
2 1 biimpi 
 |-  ( R Or A -> `' R Or A )