Theorem equequ2 2059

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 2055	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2056	. 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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  sbjust  2098  sbequ  2120  sb6  2122  equsb3r  2141  ax13lem2  2406  dveeq2ALT  2484  sb4b  2505  mojust  2564  mof  2589  eujust  2597  eujustALT  2598  eu6lem  2599  euf  2602  eleq1w  2844  mo2icl  3672  disjxun  5101  axrep2  5235  dtruALT2  5332  zfpair  5383  dfid3  5549  solin  5586  isso2i  5596  dff13f  7257  dfwe2  7786  poxp2  8153  poxp3  8160  aceq0  10190  zfac  10531  axpowndlem4  10678  zfcndac  10697  injresinj  13919  infpn2  17084  ramub1lem2  17198  fullestrcsetc  18318  fullsetcestrc  18333  symgextf1  19628  mplcoe1  22339  evlslem2  22381  mamulid  22749  mamurid  22750  mdetdiagid  22908  dscmet  24884  lgseisenlem2  27696  dchrisumlem3  27811  frgr2wwlk1  30923  sbequbidv  36983  cbvsbdavw2  37024  axtcond  37246  dfttc4  37298  mh-setindnd  37305  bj-ssblem1  37533  bj-ssblem2  37534  bj-ax12  37536  wl-aleq  38447  wl-mo2df  38482  wl-eudf  38484  wl-euequf  38486  wl-mo2t  38487  dveeq2-o  39970  axc11n-16  39975  ax12eq  39978  ax12inda  39985  ax12v2-o  39986  aks6d1c6lem3  43202  fsuppind  43598  eu6w  43667  fphpd  43802  iotavalb  45399  disjinfi  46176  eusnsn  48065  fcoresf1  48108  2reu8i  48152  2reuimp0  48153  ichexmpl1  48520  nprmmul3  48580