Theorem equequ1 1705

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

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equveli  1752  drsb1  1792  equsb3lem  1943  euequ1  2114  axext3  2153  cbvreuvw  2702  reu6  2919  reu7  2925  disjiun  3984  cbviota  5165  dff13f  5749  poxp  6211  dcdifsnid  6483  supmoti  6970  isoti  6984  nninfwlpoim  7154  exmidontriimlem3  7200  exmidontriim  7202  fsum2dlemstep  11397  ennnfonelemr  12378  ctinf  12385  reap0  14090