Theorem equequ1 1726

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 1518	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1723	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1773  drsb1  1813  equsb3lem  1969  euequ1  2140  axext3  2179  cbvreuvw  2735  reu6  2953  reu7  2959  disjiun  4029  cbviota  5225  dff13f  5820  poxp  6299  dcdifsnid  6571  supmoti  7068  isoti  7082  nninfwlpoim  7254  exmidontriimlem3  7308  exmidontriim  7310  netap  7339  fsum2dlemstep  11618  ennnfonelemr  12667  ctinf  12674  reap0  15815