Theorem equequ1 1692

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 1484	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1689	. 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 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equveli  1739  drsb1  1779  equsb3lem  1930  euequ1  2101  axext3  2140  cbvreuvw  2686  reu6  2901  reu7  2907  disjiun  3960  cbviota  5137  dff13f  5715  poxp  6173  dcdifsnid  6444  supmoti  6929  isoti  6943  exmidontriimlem3  7141  exmidontriim  7143  fsum2dlemstep  11313  ennnfonelemr  12124  ctinf  12131  reap0  13591