Theorem equequ2 1735

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 1732	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equtrr 1732	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	2	equcoms 1730	. 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 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1842  ax11v  1849  ax11ev  1850  equs5or  1852  eujust  2055  euf  2058  mo23  2094  eleq1w  2265  cbvabw  2327  csbcow  3103  disjiun  4038  iotaval  5240  dffun4f  5284  dff13f  5829  supmoti  7077  isoti  7091  nninfwlpoim  7263  exmidontriim  7319  netap  7348  ennnfonelemr  12713  ctinf  12720  infpn2  12746  lgseisenlem2  15466