Theorem equequ1 1759

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 1552	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1756	. 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1806  drsb1  1846  equsb3lem  2002  euequ1  2174  axext3  2213  cbvreuvw  2772  reu6  2994  reu7  3000  reu8nf  3112  disjiun  4084  cbviota  5293  dff13f  5916  poxp  6402  dcdifsnid  6677  modom  6999  supmoti  7197  isoti  7211  nninfwlpoim  7383  exmidontriimlem3  7443  exmidontriim  7445  netap  7478  fsum2dlemstep  12018  ennnfonelemr  13067  ctinf  13074  reap0  16730