Theorem equequ1 1736

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 1528	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 1733	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equveli  1783  drsb1  1823  equsb3lem  1979  euequ1  2150  axext3  2189  cbvreuvw  2745  reu6  2963  reu7  2969  disjiun  4042  cbviota  5242  dff13f  5846  poxp  6325  dcdifsnid  6597  supmoti  7102  isoti  7116  nninfwlpoim  7288  exmidontriimlem3  7342  exmidontriim  7344  netap  7373  fsum2dlemstep  11789  ennnfonelemr  12838  ctinf  12845  reap0  16071