Theorem equequ2 1737

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 1734	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equtrr 1734	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	2	equcoms 1732	. 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 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:  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  eujust  2057  euf  2060  mo23  2096  eleq1w  2267  cbvabw  2329  csbcow  3108  disjiun  4049  iotaval  5257  dffun4f  5301  dff13f  5857  supmoti  7116  isoti  7130  nninfwlpoim  7302  exmidontriim  7363  netap  7396  ennnfonelemr  12879  ctinf  12886  infpn2  12912  lgseisenlem2  15633