Theorem equequ2 2025

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 2021	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2022	. 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 2007

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

This theorem is referenced by:  sbjust  2063  sbequ  2083  sb6  2085  equsb3r  2104  ax13lem2  2381  dveeq2ALT  2459  sb4b  2480  mojust  2539  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  eleq1w  2824  mo2icl  3720  disjxun  5141  axrep2  5282  dtruALT2  5370  zfpair  5421  dtruOLD  5446  dfid3  5581  solin  5619  isso2i  5629  iotavalOLD  6535  dff13f  7276  dfwe2  7794  poxp2  8168  poxp3  8175  aceq0  10158  zfac  10500  axpowndlem4  10640  zfcndac  10659  injresinj  13827  infpn2  16951  ramub1lem2  17065  fullestrcsetc  18196  fullsetcestrc  18211  symgextf1  19439  mplcoe1  22055  evlslem2  22103  mamulid  22447  mamurid  22448  mdetdiagid  22606  dscmet  24585  lgseisenlem2  27420  dchrisumlem3  27535  frgr2wwlk1  30348  sbequbidv  36215  cbvsbdavw2  36256  bj-ssblem1  36655  bj-ssblem2  36656  bj-ax12  36658  wl-aleq  37536  wl-mo2df  37571  wl-eudf  37573  wl-euequf  37575  wl-mo2t  37576  dveeq2-o  38934  axc11n-16  38939  ax12eq  38942  ax12inda  38949  ax12v2-o  38950  aks6d1c6lem3  42173  fsuppind  42600  eu6w  42686  fphpd  42827  iotavalb  44449  disjinfi  45197  eusnsn  47038  fcoresf1  47081  2reu8i  47125  2reuimp0  47126  ichexmpl1  47456