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  2004  euequ1  2176  axext3  2215  cbvreuvw  2783  reu6  3005  reu7  3011  reu8nf  3123  disjiun  4103  cbviota  5316  dff13f  5942  poxp  6427  dcdifsnid  6736  modom  7060  supmoti  7283  isoti  7297  nninfwlpoim  7469  exmidontriimlem3  7529  exmidontriim  7531  netap  7564  fsum2dlemstep  12113  ennnfonelemr  13163  ctinf  13170  reap0  16830