Theorem equequ1 1758

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 1550	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1755	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1805  drsb1  1845  equsb3lem  2001  euequ1  2173  axext3  2212  cbvreuvw  2771  reu6  2993  reu7  2999  reu8nf  3111  disjiun  4081  cbviota  5289  dff13f  5906  poxp  6392  dcdifsnid  6667  modom  6989  supmoti  7186  isoti  7200  nninfwlpoim  7372  exmidontriimlem3  7431  exmidontriim  7433  netap  7466  fsum2dlemstep  11988  ennnfonelemr  13037  ctinf  13044  reap0  16612