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  2949  reu7  2955  disjiun  4024  cbviota  5220  dff13f  5813  poxp  6285  dcdifsnid  6557  supmoti  7052  isoti  7066  nninfwlpoim  7237  exmidontriimlem3  7283  exmidontriim  7285  netap  7314  fsum2dlemstep  11577  ennnfonelemr  12580  ctinf  12587  reap0  15548