Theorem equequ2 2058

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  sbjust  2097  sbequ  2119  sb6  2121  equsb3r  2140  ax13lem2  2405  dveeq2ALT  2483  sb4b  2504  mojust  2563  mof  2588  eujust  2596  eujustALT  2597  eu6lem  2598  euf  2601  eleq1w  2843  mo2icl  3671  disjxun  5100  axrep2  5234  dtruALT2  5331  zfpair  5382  dfid3  5548  solin  5585  isso2i  5595  dff13f  7259  dfwe2  7788  poxp2  8160  poxp3  8167  aceq0  10198  zfac  10539  axpowndlem4  10686  zfcndac  10705  injresinj  13927  infpn2  17092  ramub1lem2  17206  fullestrcsetc  18326  fullsetcestrc  18341  symgextf1  19636  mplcoe1  22347  evlslem2  22389  mamulid  22757  mamurid  22758  mdetdiagid  22916  dscmet  24892  lgseisenlem2  27704  dchrisumlem3  27819  frgr2wwlk1  30931  sbequbidv  37046  cbvsbdavw2  37087  axtcond  37309  dfttc4  37361  mh-setindnd  37368  bj-ssblem1  37596  bj-ssblem2  37597  bj-ax12  37599  wl-aleq  38511  wl-mo2df  38546  wl-eudf  38548  wl-euequf  38550  wl-mo2t  38551  dveeq2-o  40034  axc11n-16  40039  ax12eq  40042  ax12inda  40049  ax12v2-o  40050  aks6d1c6lem3  43266  fsuppind  43662  eu6w  43731  fphpd  43867  iotavalb  45458  disjinfi  46251  eusnsn  48140  fcoresf1  48183  2reu8i  48227  2reuimp0  48228  ichexmpl1  48595  nprmmul3  48655