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  2375  dveeq2ALT  2453  sb4b  2474  mojust  2533  mof  2557  eujust  2565  eujustALT  2566  eu6lem  2567  euf  2570  eleq1w  2812  mo2icl  3688  disjxun  5108  axrep2  5240  dtruALT2  5328  zfpair  5379  dtruOLD  5404  dfid3  5539  solin  5576  isso2i  5586  iotavalOLD  6488  dff13f  7233  dfwe2  7753  poxp2  8125  poxp3  8132  aceq0  10078  zfac  10420  axpowndlem4  10560  zfcndac  10579  injresinj  13756  infpn2  16891  ramub1lem2  17005  fullestrcsetc  18119  fullsetcestrc  18134  symgextf1  19358  mplcoe1  21951  evlslem2  21993  mamulid  22335  mamurid  22336  mdetdiagid  22494  dscmet  24467  lgseisenlem2  27294  dchrisumlem3  27409  frgr2wwlk1  30265  sbequbidv  36209  cbvsbdavw2  36250  bj-ssblem1  36649  bj-ssblem2  36650  bj-ax12  36652  wl-aleq  37530  wl-mo2df  37565  wl-eudf  37567  wl-euequf  37569  wl-mo2t  37570  dveeq2-o  38933  axc11n-16  38938  ax12eq  38941  ax12inda  38948  ax12v2-o  38949  aks6d1c6lem3  42167  fsuppind  42585  eu6w  42671  fphpd  42811  iotavalb  44426  disjinfi  45193  eusnsn  47031  fcoresf1  47074  2reu8i  47118  2reuimp0  47119  ichexmpl1  47474