Theorem equequ1 1726

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 1518	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1723	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1773  drsb1  1813  equsb3lem  1969  euequ1  2140  axext3  2179  cbvreuvw  2735  reu6  2953  reu7  2959  disjiun  4028  cbviota  5224  dff13f  5817  poxp  6290  dcdifsnid  6562  supmoti  7059  isoti  7073  nninfwlpoim  7244  exmidontriimlem3  7290  exmidontriim  7292  netap  7321  fsum2dlemstep  11599  ennnfonelemr  12640  ctinf  12647  reap0  15702