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  7261  dfwe2  7790  poxp2  8164  poxp3  8171  aceq0  10202  zfac  10543  axpowndlem4  10690  zfcndac  10709  injresinj  13931  infpn2  17098  ramub1lem2  17212  fullestrcsetc  18332  fullsetcestrc  18347  symgextf1  19642  mplcoe1  22353  evlslem2  22395  mamulid  22763  mamurid  22764  mdetdiagid  22922  dscmet  24898  lgseisenlem2  27710  dchrisumlem3  27825  frgr2wwlk1  30937  sbequbidv  37097  cbvsbdavw2  37138  axtcond  37360  dfttc4  37412  mh-setindnd  37419  bj-ssblem1  37647  bj-ssblem2  37648  bj-ax12  37650  wl-aleq  38574  wl-mo2df  38609  wl-eudf  38611  wl-euequf  38613  wl-mo2t  38614  dveeq2-o  40097  axc11n-16  40102  ax12eq  40105  ax12inda  40112  ax12v2-o  40113  aks6d1c6lem3  43329  fsuppind  43725  eu6w  43794  fphpd  43930  iotavalb  45521  disjinfi  46314  eusnsn  48203  fcoresf1  48246  2reu8i  48290  2reuimp0  48291  ichexmpl1  48658  nprmmul3  48718