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  2378  dveeq2ALT  2456  sb4b  2477  mojust  2536  mof  2561  eujust  2569  eujustALT  2570  eu6lem  2571  euf  2574  eleq1w  2817  mo2icl  3670  disjxun  5094  axrep2  5225  dtruALT2  5313  zfpair  5364  dfid3  5520  solin  5557  isso2i  5567  dff13f  7199  dfwe2  7717  poxp2  8083  poxp3  8090  aceq0  10026  zfac  10368  axpowndlem4  10509  zfcndac  10528  injresinj  13705  infpn2  16839  ramub1lem2  16953  fullestrcsetc  18072  fullsetcestrc  18087  symgextf1  19348  mplcoe1  21990  evlslem2  22032  mamulid  22383  mamurid  22384  mdetdiagid  22542  dscmet  24514  lgseisenlem2  27341  dchrisumlem3  27456  frgr2wwlk1  30353  sbequbidv  36357  cbvsbdavw2  36398  bj-ssblem1  36798  bj-ssblem2  36799  bj-ax12  36801  wl-aleq  37679  wl-mo2df  37714  wl-eudf  37716  wl-euequf  37718  wl-mo2t  37719  dveeq2-o  39132  axc11n-16  39137  ax12eq  39140  ax12inda  39147  ax12v2-o  39148  aks6d1c6lem3  42365  fsuppind  42775  eu6w  42861  fphpd  43000  iotavalb  44613  disjinfi  45378  eusnsn  47214  fcoresf1  47257  2reu8i  47301  2reuimp0  47302  ichexmpl1  47657