This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑅 Or 𝐴 → ◡ 𝑅 Or 𝐴 )

Proof

Step Hyp Ref Expression
1 cnvso ⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
2 1 biimpi ⊢ ( 𝑅 Or 𝐴 → ◡ 𝑅 Or 𝐴 )