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  2142  ax13lem2  2410  dveeq2ALT  2488  sb4b  2509  mojust  2568  mof  2593  eujust  2601  eujustALT  2602  eu6lem  2603  euf  2606  eleq1w  2848  mo2icl  3679  disjxun  5109  axrep2  5243  dtruALT2  5343  zfpair  5394  dfid3  5561  solin  5598  isso2i  5608  dff13f  7258  dfwe2  7779  poxp2  8145  poxp3  8152  aceq0  10118  zfac  10459  axpowndlem4  10600  zfcndac  10619  injresinj  13837  infpn2  16995  ramub1lem2  17109  fullestrcsetc  18229  fullsetcestrc  18244  symgextf1  19535  mplcoe1  22238  evlslem2  22280  mamulid  22648  mamurid  22649  mdetdiagid  22807  dscmet  24780  lgseisenlem2  27591  dchrisumlem3  27706  frgr2wwlk1  30751  sbequbidv  36783  cbvsbdavw2  36824  axtcond  37046  dfttc4  37098  mh-setindnd  37105  bj-ssblem1  37333  bj-ssblem2  37334  bj-ax12  37336  wl-aleq  38247  wl-mo2df  38282  wl-eudf  38284  wl-euequf  38286  wl-mo2t  38287  dveeq2-o  39765  axc11n-16  39770  ax12eq  39773  ax12inda  39780  ax12v2-o  39781  aks6d1c6lem3  42997  fsuppind  43380  eu6w  43466  fphpd  43601  iotavalb  45198  disjinfi  45968  eusnsn  47821  fcoresf1  47864  2reu8i  47908  2reuimp0  47909  ichexmpl1  48276  nprmmul3  48336