Theorem equequ2 2027

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 2023	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2024	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  sbjust  2066  sbequ  2088  sb6  2090  equsb3r  2109  ax13lem2  2380  dveeq2ALT  2458  sb4b  2479  mojust  2538  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  eleq1w  2819  mo2icl  3672  disjxun  5096  axrep2  5227  dtruALT2  5315  zfpair  5366  dfid3  5522  solin  5559  isso2i  5569  dff13f  7201  dfwe2  7719  poxp2  8085  poxp3  8092  aceq0  10028  zfac  10370  axpowndlem4  10511  zfcndac  10530  injresinj  13707  infpn2  16841  ramub1lem2  16955  fullestrcsetc  18074  fullsetcestrc  18089  symgextf1  19350  mplcoe1  21992  evlslem2  22034  mamulid  22385  mamurid  22386  mdetdiagid  22544  dscmet  24516  lgseisenlem2  27343  dchrisumlem3  27458  frgr2wwlk1  30404  sbequbidv  36408  cbvsbdavw2  36449  mh-setindnd  36667  bj-ssblem1  36855  bj-ssblem2  36856  bj-ax12  36858  wl-aleq  37740  wl-mo2df  37775  wl-eudf  37777  wl-euequf  37779  wl-mo2t  37780  dveeq2-o  39193  axc11n-16  39198  ax12eq  39201  ax12inda  39208  ax12v2-o  39209  aks6d1c6lem3  42426  fsuppind  42833  eu6w  42919  fphpd  43058  iotavalb  44671  disjinfi  45436  eusnsn  47272  fcoresf1  47315  2reu8i  47359  2reuimp0  47360  ichexmpl1  47715