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 𝐴 )