Theorem equequ2 2029

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  sbjust  2066  sbequ  2086  sb6  2088  equsb3r  2102  ax13lem2  2375  dveeq2ALT  2453  sb4b  2474  mojust  2533  mof  2557  eujust  2565  eujustALT  2566  eu6lem  2567  euf  2570  eleq1w  2816  mo2icl  3710  disjxun  5146  axrep2  5288  dtruALT2  5368  zfpair  5419  dtruOLD  5441  dfid3  5577  solin  5613  isso2i  5623  iotavalOLD  6517  dff13f  7257  dfwe2  7763  poxp2  8131  poxp3  8138  aceq0  10115  zfac  10457  axpowndlem4  10597  zfcndac  10616  injresinj  13757  infpn2  16850  ramub1lem2  16964  fullestrcsetc  18107  fullsetcestrc  18122  symgextf1  19330  mplcoe1  21811  evlslem2  21861  mamulid  22163  mamurid  22164  mdetdiagid  22322  dscmet  24301  lgseisenlem2  27103  dchrisumlem3  27218  frgr2wwlk1  29837  bj-ssblem1  35834  bj-ssblem2  35835  bj-ax12  35837  wl-aleq  36707  wl-mo2df  36738  wl-eudf  36740  wl-euequf  36742  wl-mo2t  36743  dveeq2-o  38106  axc11n-16  38111  ax12eq  38114  ax12inda  38121  ax12v2-o  38122  fsuppind  41464  fphpd  41856  iotavalb  43491  disjinfi  44190  eusnsn  46035  fcoresf1  46078  2reu8i  46120  2reuimp0  46121  ichexmpl1  46436