Theorem equequ1 1723

Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)

Assertion

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

Proof of Theorem equequ1

Step	Hyp	Ref	Expression
1		ax-8 1515	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1720	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
3	1, 2	impbid 129	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1770  drsb1  1810  equsb3lem  1966  euequ1  2137  axext3  2176  cbvreuvw  2732  reu6  2950  reu7  2956  disjiun  4025  cbviota  5221  dff13f  5814  poxp  6287  dcdifsnid  6559  supmoti  7054  isoti  7068  nninfwlpoim  7239  exmidontriimlem3  7285  exmidontriim  7287  netap  7316  fsum2dlemstep  11580  ennnfonelemr  12583  ctinf  12590  reap0  15618