Theorem equequ2 1706

Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
equequ2	⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Proof of Theorem equequ2

Step	Hyp	Ref	Expression
1		equtrr 1703	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equtrr 1703	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	2	equcoms 1701	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
4	1, 3	impbid 128	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax11v2  1813  ax11v  1820  ax11ev  1821  equs5or  1823  eujust  2021  euf  2024  mo23  2060  eleq1w  2231  cbvabw  2293  csbcow  3060  disjiun  3984  iotaval  5171  dffun4f  5214  dff13f  5749  supmoti  6970  isoti  6984  nninfwlpoim  7154  exmidontriim  7202  ennnfonelemr  12378  ctinf  12385  infpn2  12411