Theorem equcomi1

Description: Proof of equcomi from equid1 , avoiding use of ax-5 (the only use of ax-5 is via ax7 , so using ax-7 instead would remove dependency on ax-5 ). (Contributed by BJ, 8-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	equcomi1	$$⊢x=y\to y=x$$

Proof

Step	Hyp	Ref	Expression
1		equid1	$$⊢x=x$$
2		ax7	$$⊢x=y\to \left(x=x\to y=x\right)$$
3	1 2	mpi	$$⊢x=y\to y=x$$