Theorem equequ2 2056

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  sbjust  2095  sbequ  2117  sb6  2119  equsb3r  2139  ax13lem2  2408  dveeq2ALT  2486  sb4b  2507  mojust  2566  mof  2591  eujust  2599  eujustALT  2600  eu6lem  2601  euf  2604  eleq1w  2846  mo2icl  3677  disjxun  5107  axrep2  5241  dtruALT2  5341  zfpair  5392  dfid3  5559  solin  5596  isso2i  5606  dff13f  7253  dfwe2  7769  poxp2  8135  poxp3  8142  aceq0  10098  zfac  10439  axpowndlem4  10580  zfcndac  10599  injresinj  13816  infpn2  16968  ramub1lem2  17082  fullestrcsetc  18202  fullsetcestrc  18217  symgextf1  19486  mplcoe1  22188  evlslem2  22230  mamulid  22598  mamurid  22599  mdetdiagid  22757  dscmet  24729  lgseisenlem2  27540  dchrisumlem3  27655  frgr2wwlk1  30680  sbequbidv  36726  cbvsbdavw2  36767  axtcond  36989  dfttc4  37041  mh-setindnd  37048  bj-ssblem1  37276  bj-ssblem2  37277  bj-ax12  37279  wl-aleq  38190  wl-mo2df  38225  wl-eudf  38227  wl-euequf  38229  wl-mo2t  38230  dveeq2-o  39707  axc11n-16  39712  ax12eq  39715  ax12inda  39722  ax12v2-o  39723  aks6d1c6lem3  42939  fsuppind  43322  eu6w  43408  fphpd  43543  iotavalb  45140  disjinfi  45910  eusnsn  47763  fcoresf1  47806  2reu8i  47850  2reuimp0  47851  ichexmpl1  48218  nprmmul3  48278