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  2380  dveeq2ALT  2458  sb4b  2479  mojust  2538  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  eleq1w  2819  mo2icl  3660  disjxun  5083  axrep2  5215  dtruALT2  5312  zfpair  5363  dfid3  5529  solin  5566  isso2i  5576  dff13f  7210  dfwe2  7728  poxp2  8093  poxp3  8100  aceq0  10040  zfac  10382  axpowndlem4  10523  zfcndac  10542  injresinj  13746  infpn2  16884  ramub1lem2  16998  fullestrcsetc  18117  fullsetcestrc  18132  symgextf1  19396  mplcoe1  22015  evlslem2  22057  mamulid  22406  mamurid  22407  mdetdiagid  22565  dscmet  24537  lgseisenlem2  27339  dchrisumlem3  27454  frgr2wwlk1  30399  sbequbidv  36396  cbvsbdavw2  36437  axtcond  36660  dfttc4  36712  mh-setindnd  36719  bj-ssblem1  36948  bj-ssblem2  36949  bj-ax12  36951  wl-aleq  37860  wl-mo2df  37895  wl-eudf  37897  wl-euequf  37899  wl-mo2t  37900  dveeq2-o  39379  axc11n-16  39384  ax12eq  39387  ax12inda  39394  ax12v2-o  39395  aks6d1c6lem3  42611  fsuppind  43023  eu6w  43109  fphpd  43244  iotavalb  44857  disjinfi  45622  eusnsn  47474  fcoresf1  47517  2reu8i  47561  2reuimp0  47562  ichexmpl1  47929  nprmmul3  47989