Theorem equequ1 1671

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 1465	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1668	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
3	1, 2	impbid 128	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ie2 1453  ax-8 1465  ax-17 1489  ax-i9 1493

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equveli  1715  drsb1  1753  equsb3lem  1899  euequ1  2070  axext3  2098  reu6  2842  reu7  2848  disjiun  3890  cbviota  5051  dff13f  5625  poxp  6083  dcdifsnid  6354  supmoti  6832  isoti  6846  fsum2dlemstep  11095  ennnfonelemr  11781  ctinf  11788