Theorem equequ2 1953

Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.)

Assertion

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

Proof of Theorem equequ2

Step	Hyp	Ref	Expression
1		equtrr 1949	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 1950	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	1, 2	impbid 202	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  axc11nlemOLD2  1988  ax12vOLDOLD  2051  axc11nlemOLD  2160  ax13lem2  2296  axc15  2303  axc11nlemALT  2306  dveeq2ALT  2340  ax12v2OLD  2342  eujust  2472  eujustALT  2473  euequ1  2476  euf  2478  mo2  2479  eleq1w  2684  disjxun  4651  axrep2  4773  dtru  4857  zfpair  4904  dfid3  5025  isso2i  5067  iotaval  5862  dff13f  6513  dfwe2  6981  aceq0  8941  zfac  9282  axpowndlem4  9422  zfcndac  9441  injresinj  12589  infpn2  15617  ramub1lem2  15731  fullestrcsetc  16791  fullsetcestrc  16806  symgextf1  17841  mplcoe1  19465  evlslem2  19512  mamulid  20247  mamurid  20248  mdetdiagid  20406  dscmet  22377  lgseisenlem2  25101  dchrisumlem3  25180  frgr2wwlk1  27193  bj-ssbjust  32618  bj-ssbequ  32629  bj-ssblem1  32630  bj-ssblem2  32631  bj-ssb1a  32632  bj-ssb1  32633  bj-ssbcom3lem  32650  bj-axrep2  32789  bj-dtru  32797  bj-ax8  32887  wl-aleq  33322  wl-mo2df  33352  wl-eudf  33354  wl-euequ1f  33356  wl-mo2t  33357  dveeq2-o  34218  axc11n-16  34223  ax12eq  34226  ax12inda  34233  ax12v2-o  34234  fphpd  37380  iotavalb  38631  disjinfi  39380