This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (x = x \to y = x)$
3	1 2	mpi	$⊢ x = y \to y = x$