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  3682  disjxun  5100  axrep2  5232  dtruALT2  5320  zfpair  5371  dtruOLD  5396  dfid3  5529  solin  5566  isso2i  5576  iotavalOLD  6473  dff13f  7212  dfwe2  7730  poxp2  8099  poxp3  8106  aceq0  10047  zfac  10389  axpowndlem4  10529  zfcndac  10548  injresinj  13725  infpn2  16860  ramub1lem2  16974  fullestrcsetc  18088  fullsetcestrc  18103  symgextf1  19327  mplcoe1  21920  evlslem2  21962  mamulid  22304  mamurid  22305  mdetdiagid  22463  dscmet  24436  lgseisenlem2  27263  dchrisumlem3  27378  frgr2wwlk1  30231  sbequbidv  36175  cbvsbdavw2  36216  bj-ssblem1  36615  bj-ssblem2  36616  bj-ax12  36618  wl-aleq  37496  wl-mo2df  37531  wl-eudf  37533  wl-euequf  37535  wl-mo2t  37536  dveeq2-o  38899  axc11n-16  38904  ax12eq  38907  ax12inda  38914  ax12v2-o  38915  aks6d1c6lem3  42133  fsuppind  42551  eu6w  42637  fphpd  42777  iotavalb  44392  disjinfi  45159  eusnsn  47000  fcoresf1  47043  2reu8i  47087  2reuimp0  47088  ichexmpl1  47443