Theorem equequ1

Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993) (Proof shortened by Wolf Lammen, 10-Dec-2017)

	Ref	Expression
Assertion	equequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ax7	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )
2		equtr	⊢ ( 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → 𝑥 = 𝑧 ) )
3	1 2	impbid	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑦 = 𝑧 ) )