Theorem equequ1 1760

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 1553	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1757	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1808  drsb1  1848  equsb3lem  2006  euequ1  2178  axext3  2217  cbvreuvw  2786  reu6  3008  reu7  3014  reu8nf  3126  disjiun  4106  cbviota  5319  dff13f  5945  poxp  6430  dcdifsnid  6739  modom  7063  supmoti  7286  isoti  7300  nninfwlpoim  7472  exmidontriimlem3  7532  exmidontriim  7534  netap  7573  fsum2dlemstep  12128  ennnfonelemr  13195  ctinf  13202  reap0  16892