Theorem equequ2 2030

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 2026	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2027	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  sbjust  2067  sbequ  2087  sb6  2089  equsb3r  2103  ax13lem2  2376  dveeq2ALT  2454  sb4b  2475  mojust  2534  mof  2558  eujust  2566  eujustALT  2567  eu6lem  2568  euf  2571  eleq1w  2817  mo2icl  3711  disjxun  5147  axrep2  5289  dtruALT2  5369  zfpair  5420  dtruOLD  5442  dfid3  5578  solin  5614  isso2i  5624  iotavalOLD  6518  dff13f  7255  dfwe2  7761  poxp2  8129  poxp3  8136  aceq0  10113  zfac  10455  axpowndlem4  10595  zfcndac  10614  injresinj  13753  infpn2  16846  ramub1lem2  16960  fullestrcsetc  18103  fullsetcestrc  18118  symgextf1  19289  mplcoe1  21592  evlslem2  21642  mamulid  21943  mamurid  21944  mdetdiagid  22102  dscmet  24081  lgseisenlem2  26879  dchrisumlem3  26994  frgr2wwlk1  29582  bj-ssblem1  35531  bj-ssblem2  35532  bj-ax12  35534  wl-aleq  36404  wl-mo2df  36435  wl-eudf  36437  wl-euequf  36439  wl-mo2t  36440  dveeq2-o  37803  axc11n-16  37808  ax12eq  37811  ax12inda  37818  ax12v2-o  37819  fsuppind  41162  fphpd  41554  iotavalb  43189  disjinfi  43891  eusnsn  45736  fcoresf1  45779  2reu8i  45821  2reuimp0  45822  ichexmpl1  46137