Metamath Proof Explorer
Description: Deduction form of equcom , symmetry of equality. For the versions for
classes, see eqcom and eqcomd . (Contributed by BJ, 6Oct2019)


Ref 
Expression 

Hypothesis 
equcomd.1 
$${\u22a2}{\phi}\to {x}={y}$$ 

Assertion 
equcomd 
$${\u22a2}{\phi}\to {y}={x}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

equcomd.1 
$${\u22a2}{\phi}\to {x}={y}$$ 
2 

equcom 
$${\u22a2}{x}={y}\leftrightarrow {y}={x}$$ 
3 
1 2

sylib 
$${\u22a2}{\phi}\to {y}={x}$$ 