Theorem equequ1 1764

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This proof depends on definitions:  df-bi 117

This theorem is used by:  equveli  1812  drsb1  1852  equsb3lem  2010  euequ1  2182  axext3  2221  cbvreuvw  2792  reu6  3015  reu7  3021  reu8nf  3133  disjiun  4125  cbviota  5345  dff13f  5979  poxp  6472  dcdifsnid  6781  modom  7113  supmoti  7340  isoti  7354  nninfwlpoim  7526  exmidontriimlem3  7586  exmidontriim  7588  netap  7627  fsum2dlemstep  12227  ennnfonelemr  13373  ctinf  13380  reap0  17327