Theorem equequ1 1760

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 1757	. 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  1807  drsb1  1847  equsb3lem  2003  euequ1  2175  axext3  2214  cbvreuvw  2773  reu6  2995  reu7  3001  reu8nf  3113  disjiun  4083  cbviota  5291  dff13f  5911  poxp  6397  dcdifsnid  6672  modom  6994  supmoti  7192  isoti  7206  nninfwlpoim  7378  exmidontriimlem3  7438  exmidontriim  7440  netap  7473  fsum2dlemstep  11997  ennnfonelemr  13046  ctinf  13053  reap0  16683