Theorem equequ2 2026

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 2022	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2023	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  sbjust  2064  sbequ  2084  sb6  2086  equsb3r  2105  ax13lem2  2374  dveeq2ALT  2452  sb4b  2473  mojust  2532  mof  2556  eujust  2564  eujustALT  2565  eu6lem  2566  euf  2569  eleq1w  2811  mo2icl  3674  disjxun  5090  axrep2  5221  dtruALT2  5309  zfpair  5360  dfid3  5517  solin  5554  isso2i  5564  dff13f  7192  dfwe2  7710  poxp2  8076  poxp3  8083  aceq0  10012  zfac  10354  axpowndlem4  10494  zfcndac  10513  injresinj  13691  infpn2  16825  ramub1lem2  16939  fullestrcsetc  18057  fullsetcestrc  18072  symgextf1  19300  mplcoe1  21942  evlslem2  21984  mamulid  22326  mamurid  22327  mdetdiagid  22485  dscmet  24458  lgseisenlem2  27285  dchrisumlem3  27400  frgr2wwlk1  30273  sbequbidv  36188  cbvsbdavw2  36229  bj-ssblem1  36628  bj-ssblem2  36629  bj-ax12  36631  wl-aleq  37509  wl-mo2df  37544  wl-eudf  37546  wl-euequf  37548  wl-mo2t  37549  dveeq2-o  38912  axc11n-16  38917  ax12eq  38920  ax12inda  38927  ax12v2-o  38928  aks6d1c6lem3  42145  fsuppind  42563  eu6w  42649  fphpd  42789  iotavalb  44403  disjinfi  45170  eusnsn  47010  fcoresf1  47053  2reu8i  47097  2reuimp0  47098  ichexmpl1  47453