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	$$⊢\phi \to x=y$$
Assertion	equcomd	$$⊢\phi \to y=x$$

Proof

Step	Hyp	Ref	Expression
1		equcomd.1	$$⊢\phi \to x=y$$
2		equcom	$$⊢x=y\leftrightarrow y=x$$
3	1 2	sylib	$$⊢\phi \to y=x$$