Theorem equequ2 2028

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 2024	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2025	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  sbjust  2067  sbequ  2089  sb6  2091  equsb3r  2110  ax13lem2  2381  dveeq2ALT  2459  sb4b  2480  mojust  2539  mof  2564  eujust  2572  eujustALT  2573  eu6lem  2574  euf  2577  eleq1w  2820  mo2icl  3661  disjxun  5084  axrep2  5215  dtruALT2  5307  zfpair  5358  dfid3  5522  solin  5559  isso2i  5569  dff13f  7203  dfwe2  7721  poxp2  8086  poxp3  8093  aceq0  10031  zfac  10373  axpowndlem4  10514  zfcndac  10533  injresinj  13737  infpn2  16875  ramub1lem2  16989  fullestrcsetc  18108  fullsetcestrc  18123  symgextf1  19387  mplcoe1  22025  evlslem2  22067  mamulid  22416  mamurid  22417  mdetdiagid  22575  dscmet  24547  lgseisenlem2  27353  dchrisumlem3  27468  frgr2wwlk1  30414  sbequbidv  36412  cbvsbdavw2  36453  axtcond  36676  dfttc4  36728  mh-setindnd  36735  bj-ssblem1  36964  bj-ssblem2  36965  bj-ax12  36967  wl-aleq  37874  wl-mo2df  37909  wl-eudf  37911  wl-euequf  37913  wl-mo2t  37914  dveeq2-o  39393  axc11n-16  39398  ax12eq  39401  ax12inda  39408  ax12v2-o  39409  aks6d1c6lem3  42625  fsuppind  43037  eu6w  43123  fphpd  43262  iotavalb  44875  disjinfi  45640  eusnsn  47486  fcoresf1  47529  2reu8i  47573  2reuimp0  47574  ichexmpl1  47941  nprmmul3  48001