Theorem equequ2 1761

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 1758	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equtrr 1758	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	2	equcoms 1756	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
4	1, 3	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:  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  eujust  2084  euf  2087  mo23  2124  eleq1w  2295  cbvabw  2359  csbcow  3152  disjiun  4109  iotaval  5329  dffun4f  5373  dff13f  5949  modom  7074  supmoti  7297  isoti  7311  nninfwlpoim  7483  exmidontriim  7545  netap  7584  ennnfonelemr  13258  ctinf  13265  infpn2  13291  lgseisenlem2  16070