Theorem equequ2 2021

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 2017	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2018	. 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 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774

This theorem is referenced by:  sbjust  2058  sbequ  2078  sb6  2080  equsb3r  2094  ax13lem2  2369  dveeq2ALT  2447  sb4b  2468  mojust  2527  mof  2551  eujust  2559  eujustALT  2560  eu6lem  2561  euf  2564  eleq1w  2808  mo2icl  3706  disjxun  5147  axrep2  5289  dtruALT2  5370  zfpair  5421  dtruOLD  5443  dfid3  5579  solin  5615  isso2i  5625  iotavalOLD  6523  dff13f  7266  dfwe2  7777  poxp2  8148  poxp3  8155  aceq0  10148  zfac  10490  axpowndlem4  10630  zfcndac  10649  injresinj  13794  infpn2  16890  ramub1lem2  17004  fullestrcsetc  18150  fullsetcestrc  18165  symgextf1  19393  mplcoe1  22002  evlslem2  22052  mamulid  22392  mamurid  22393  mdetdiagid  22551  dscmet  24530  lgseisenlem2  27359  dchrisumlem3  27474  frgr2wwlk1  30216  bj-ssblem1  36263  bj-ssblem2  36264  bj-ax12  36266  wl-aleq  37135  wl-mo2df  37170  wl-eudf  37172  wl-euequf  37174  wl-mo2t  37175  dveeq2-o  38537  axc11n-16  38542  ax12eq  38545  ax12inda  38552  ax12v2-o  38553  aks6d1c6lem3  41777  fsuppind  41960  eu6w  42238  fphpd  42380  iotavalb  44011  disjinfi  44706  eusnsn  46548  fcoresf1  46591  2reu8i  46633  2reuimp0  46634  ichexmpl1  46948