Theorem equcomd

Description: Deduction form of equcom , symmetry of equality. For the versions for classes, see eqcom and eqcomd . (Contributed by BJ, 6-Oct-2019)

	Ref	Expression
Hypothesis	equcomd.1	⊢ ( 𝜑 → 𝑥 = 𝑦 )
Assertion	equcomd	⊢ ( 𝜑 → 𝑦 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		equcomd.1	⊢ ( 𝜑 → 𝑥 = 𝑦 )
2		equcom	⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
3	1 2	sylib	⊢ ( 𝜑 → 𝑦 = 𝑥 )