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	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		equid1	⊢ 𝑥 = 𝑥
2		ax7	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑥 → 𝑦 = 𝑥 ) )
3	1 2	mpi	⊢ ( 𝑥 = 𝑦 → 𝑦 = 𝑥 )