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  3685  disjxun  5105  axrep2  5237  dtruALT2  5325  zfpair  5376  dtruOLD  5401  dfid3  5536  solin  5573  isso2i  5583  iotavalOLD  6485  dff13f  7230  dfwe2  7750  poxp2  8122  poxp3  8129  aceq0  10071  zfac  10413  axpowndlem4  10553  zfcndac  10572  injresinj  13749  infpn2  16884  ramub1lem2  16998  fullestrcsetc  18112  fullsetcestrc  18127  symgextf1  19351  mplcoe1  21944  evlslem2  21986  mamulid  22328  mamurid  22329  mdetdiagid  22487  dscmet  24460  lgseisenlem2  27287  dchrisumlem3  27402  frgr2wwlk1  30258  sbequbidv  36202  cbvsbdavw2  36243  bj-ssblem1  36642  bj-ssblem2  36643  bj-ax12  36645  wl-aleq  37523  wl-mo2df  37558  wl-eudf  37560  wl-euequf  37562  wl-mo2t  37563  dveeq2-o  38926  axc11n-16  38931  ax12eq  38934  ax12inda  38941  ax12v2-o  38942  aks6d1c6lem3  42160  fsuppind  42578  eu6w  42664  fphpd  42804  iotavalb  44419  disjinfi  45186  eusnsn  47027  fcoresf1  47070  2reu8i  47114  2reuimp0  47115  ichexmpl1  47470