Theorem equequ1 1738

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 1530	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1735	. 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 1475  ax-ie2 1520  ax-8 1530  ax-17 1552  ax-i9 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1785  drsb1  1825  equsb3lem  1981  euequ1  2153  axext3  2192  cbvreuvw  2751  reu6  2972  reu7  2978  reu8nf  3090  disjiun  4057  cbviota  5259  dff13f  5867  poxp  6348  dcdifsnid  6620  supmoti  7128  isoti  7142  nninfwlpoim  7314  exmidontriimlem3  7373  exmidontriim  7375  netap  7408  fsum2dlemstep  11911  ennnfonelemr  12960  ctinf  12967  reap0  16337