Theorem equequ1 1700

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 1492	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1697	. 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 1437  ax-ie2 1482  ax-8 1492  ax-17 1514  ax-i9 1518

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equveli  1747  drsb1  1787  equsb3lem  1938  euequ1  2109  axext3  2148  cbvreuvw  2698  reu6  2915  reu7  2921  disjiun  3977  cbviota  5158  dff13f  5738  poxp  6200  dcdifsnid  6472  supmoti  6958  isoti  6972  exmidontriimlem3  7179  exmidontriim  7181  fsum2dlemstep  11375  ennnfonelemr  12356  ctinf  12363  reap0  13937