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  2380  dveeq2ALT  2458  sb4b  2479  mojust  2538  mof  2562  eujust  2570  eujustALT  2571  eu6lem  2572  euf  2575  eleq1w  2817  mo2icl  3697  disjxun  5117  axrep2  5252  dtruALT2  5340  zfpair  5391  dtruOLD  5416  dfid3  5551  solin  5588  isso2i  5598  iotavalOLD  6505  dff13f  7248  dfwe2  7768  poxp2  8142  poxp3  8149  aceq0  10132  zfac  10474  axpowndlem4  10614  zfcndac  10633  injresinj  13804  infpn2  16933  ramub1lem2  17047  fullestrcsetc  18163  fullsetcestrc  18178  symgextf1  19402  mplcoe1  21995  evlslem2  22037  mamulid  22379  mamurid  22380  mdetdiagid  22538  dscmet  24511  lgseisenlem2  27339  dchrisumlem3  27454  frgr2wwlk1  30310  sbequbidv  36232  cbvsbdavw2  36273  bj-ssblem1  36672  bj-ssblem2  36673  bj-ax12  36675  wl-aleq  37553  wl-mo2df  37588  wl-eudf  37590  wl-euequf  37592  wl-mo2t  37593  dveeq2-o  38951  axc11n-16  38956  ax12eq  38959  ax12inda  38966  ax12v2-o  38967  aks6d1c6lem3  42185  fsuppind  42613  eu6w  42699  fphpd  42839  iotavalb  44454  disjinfi  45216  eusnsn  47055  fcoresf1  47098  2reu8i  47142  2reuimp0  47143  ichexmpl1  47483