Theorem equequ2 2027

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 2023	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2024	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  sbjust  2066  sbequ  2086  sb6  2088  equsb3r  2107  ax13lem2  2376  dveeq2ALT  2454  sb4b  2475  mojust  2534  mof  2558  eujust  2566  eujustALT  2567  eu6lem  2568  euf  2571  eleq1w  2814  mo2icl  3668  disjxun  5084  axrep2  5215  dtruALT2  5303  zfpair  5354  dfid3  5509  solin  5546  isso2i  5556  dff13f  7184  dfwe2  7702  poxp2  8068  poxp3  8075  aceq0  10004  zfac  10346  axpowndlem4  10486  zfcndac  10505  injresinj  13686  infpn2  16820  ramub1lem2  16934  fullestrcsetc  18052  fullsetcestrc  18067  symgextf1  19328  mplcoe1  21967  evlslem2  22009  mamulid  22351  mamurid  22352  mdetdiagid  22510  dscmet  24482  lgseisenlem2  27309  dchrisumlem3  27424  frgr2wwlk1  30301  sbequbidv  36248  cbvsbdavw2  36289  bj-ssblem1  36688  bj-ssblem2  36689  bj-ax12  36691  wl-aleq  37569  wl-mo2df  37604  wl-eudf  37606  wl-euequf  37608  wl-mo2t  37609  dveeq2-o  38972  axc11n-16  38977  ax12eq  38980  ax12inda  38987  ax12v2-o  38988  aks6d1c6lem3  42205  fsuppind  42623  eu6w  42709  fphpd  42849  iotavalb  44463  disjinfi  45229  eusnsn  47057  fcoresf1  47100  2reu8i  47144  2reuimp0  47145  ichexmpl1  47500