Theorem equequ2 2059

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 2055	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2056	. 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 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  sbjust  2098  sbequ  2120  sb6  2122  equsb3r  2141  ax13lem2  2405  dveeq2ALT  2483  sb4b  2504  mojust  2563  mof  2588  eujust  2596  eujustALT  2597  eu6lem  2598  euf  2601  eleq1w  2843  mo2icl  3672  disjxun  5101  axrep2  5235  dtruALT2  5335  zfpair  5386  dfid3  5553  solin  5590  isso2i  5600  dff13f  7252  dfwe2  7773  poxp2  8141  poxp3  8148  aceq0  10121  zfac  10462  axpowndlem4  10609  zfcndac  10628  injresinj  13847  infpn2  17005  ramub1lem2  17119  fullestrcsetc  18239  fullsetcestrc  18254  symgextf1  19548  mplcoe1  22253  evlslem2  22295  mamulid  22663  mamurid  22664  mdetdiagid  22822  dscmet  24798  lgseisenlem2  27612  dchrisumlem3  27727  frgr2wwlk1  30809  sbequbidv  36834  cbvsbdavw2  36875  axtcond  37097  dfttc4  37149  mh-setindnd  37156  bj-ssblem1  37384  bj-ssblem2  37385  bj-ax12  37387  wl-aleq  38298  wl-mo2df  38333  wl-eudf  38335  wl-euequf  38337  wl-mo2t  38338  dveeq2-o  39806  axc11n-16  39811  ax12eq  39814  ax12inda  39821  ax12v2-o  39822  aks6d1c6lem3  43038  fsuppind  43436  eu6w  43522  fphpd  43657  iotavalb  45254  disjinfi  46024  eusnsn  47914  fcoresf1  47957  2reu8i  48001  2reuimp0  48002  ichexmpl1  48369  nprmmul3  48429