Theorem equequ2 2033

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

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  sbjust  2072  sbequ  2094  sb6  2096  equsb3r  2115  ax13lem2  2384  dveeq2ALT  2462  sb4b  2483  mojust  2542  mof  2567  eujust  2575  eujustALT  2576  eu6lem  2577  euf  2580  eleq1w  2822  mo2icl  3655  disjxun  5070  axrep2  5202  dtruALT2  5299  zfpair  5350  dfid3  5516  solin  5553  isso2i  5563  dff13f  7199  dfwe2  7717  poxp2  8083  poxp3  8090  aceq0  10031  zfac  10373  axpowndlem4  10514  zfcndac  10533  injresinj  13737  infpn2  16875  ramub1lem2  16989  fullestrcsetc  18108  fullsetcestrc  18123  symgextf1  19387  mplcoe1  22013  evlslem2  22055  mamulid  22424  mamurid  22425  mdetdiagid  22583  dscmet  24555  lgseisenlem2  27357  dchrisumlem3  27472  frgr2wwlk1  30417  sbequbidv  36442  cbvsbdavw2  36483  axtcond  36706  dfttc4  36758  mh-setindnd  36765  bj-ssblem1  36994  bj-ssblem2  36995  bj-ax12  36997  wl-aleq  37906  wl-mo2df  37941  wl-eudf  37943  wl-euequf  37945  wl-mo2t  37946  dveeq2-o  39425  axc11n-16  39430  ax12eq  39433  ax12inda  39440  ax12v2-o  39441  aks6d1c6lem3  42657  fsuppind  43040  eu6w  43126  fphpd  43261  iotavalb  44874  disjinfi  45639  eusnsn  47489  fcoresf1  47532  2reu8i  47576  2reuimp0  47577  ichexmpl1  47944  nprmmul3  48004