Theorem equequ2 2028

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 2024	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2025	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	1, 2	impbid 212	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  sbjust  2067  sbequ  2089  sb6  2091  equsb3r  2110  ax13lem2  2381  dveeq2ALT  2459  sb4b  2480  mojust  2539  mof  2564  eujust  2572  eujustALT  2573  eu6lem  2574  euf  2577  eleq1w  2820  mo2icl  3674  disjxun  5098  axrep2  5229  dtruALT2  5317  zfpair  5368  dfid3  5530  solin  5567  isso2i  5577  dff13f  7211  dfwe2  7729  poxp2  8095  poxp3  8102  aceq0  10040  zfac  10382  axpowndlem4  10523  zfcndac  10542  injresinj  13719  infpn2  16853  ramub1lem2  16967  fullestrcsetc  18086  fullsetcestrc  18101  symgextf1  19362  mplcoe1  22004  evlslem2  22046  mamulid  22397  mamurid  22398  mdetdiagid  22556  dscmet  24528  lgseisenlem2  27355  dchrisumlem3  27470  frgr2wwlk1  30416  sbequbidv  36430  cbvsbdavw2  36471  mh-setindnd  36689  bj-ssblem1  36899  bj-ssblem2  36900  bj-ax12  36902  wl-aleq  37790  wl-mo2df  37825  wl-eudf  37827  wl-euequf  37829  wl-mo2t  37830  dveeq2-o  39309  axc11n-16  39314  ax12eq  39317  ax12inda  39324  ax12v2-o  39325  aks6d1c6lem3  42542  fsuppind  42948  eu6w  43034  fphpd  43173  iotavalb  44786  disjinfi  45551  eusnsn  47386  fcoresf1  47429  2reu8i  47473  2reuimp0  47474  ichexmpl1  47829