Theorem equequ2 2061

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 2057	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2058	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	1, 2	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  sbjust  2100  sbequ  2122  sb6  2124  equsb3r  2143  ax13lem2  2408  dveeq2ALT  2486  sb4b  2507  mojust  2566  mof  2591  eujust  2599  eujustALT  2600  eu6lem  2601  euf  2604  eleq1w  2847  mo2icl  3675  disjxun  5106  axrep2  5241  dtruALT2  5339  zfpair  5390  dfid3  5556  solin  5593  isso2i  5603  dff13f  7290  dfwe2  7820  poxp2  8197  poxp3  8204  aceq0  10236  zfac  10577  axpowndlem4  10724  zfcndac  10743  injresinj  13966  infpn2  17135  ramub1lem2  17249  fullestrcsetc  18375  fullsetcestrc  18390  symgextf1  19686  mplcoe1  22401  evlslem2  22443  mamulid  22811  mamurid  22812  mdetdiagid  22970  dscmet  24946  lgseisenlem2  27760  dchrisumlem3  27875  frgr2wwlk1  30987  elpssmo  36673  sbequbidv  37218  cbvsbdavw2  37259  axtcond  37481  dfttc4  37533  mh-setindnd  37540  bj-ssblem1  37768  bj-ssblem2  37769  bj-ax12  37771  wl-aleq  38735  wl-mo2df  38770  wl-eudf  38772  wl-euequf  38774  wl-mo2t  38775  dveeq2-o  40256  axc11n-16  40261  ax12eq  40264  ax12inda  40271  ax12v2-o  40272  aks6d1c6lem3  43488  fsuppind  43884  eu6w  43953  fphpd  44089  iotavalb  45674  disjinfi  46480  eusnsn  48369  fcoresf1  48412  2reu8i  48457  2reuimp0  48458  ichexmpl1  48824  nprmmul3  48884