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	|- ( ph -> x = y )
Assertion	equcomd	|- ( ph -> y = x )

Proof

Step	Hyp	Ref	Expression
1		equcomd.1	|- ( ph -> x = y )
2		equcom	|- ( x = y <-> y = x )
3	1 2	sylib	|- ( ph -> y = x )