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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  eujust  2081  euf  2084  mo23  2121  eleq1w  2292  cbvabw  2354  csbcow  3138  disjiun  4083  iotaval  5298  dffun4f  5342  dff13f  5910  modom  6993  supmoti  7191  isoti  7205  nninfwlpoim  7377  exmidontriim  7439  netap  7472  ennnfonelemr  13043  ctinf  13050  infpn2  13076  lgseisenlem2  15799