Theorem equequ2 2032

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 2028	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2029	. 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 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786

This theorem is referenced by:  sbjust  2069  sbequ  2089  sb6  2091  equsb3r  2105  ax13lem2  2377  dveeq2ALT  2455  sb4b  2476  sb4bOLD  2477  mojust  2540  mof  2564  eujust  2572  eujustALT  2573  eu6lem  2574  euf  2577  eleq1w  2822  mo2icl  3652  disjxun  5076  axrep2  5216  dtru  5296  zfpair  5347  dfid3  5491  solin  5527  isso2i  5537  iotaval  6404  dff13f  7123  dfwe2  7615  aceq0  9858  zfac  10200  axpowndlem4  10340  zfcndac  10359  injresinj  13489  infpn2  16595  ramub1lem2  16709  fullestrcsetc  17849  fullsetcestrc  17864  symgextf1  19010  mplcoe1  21219  evlslem2  21270  mamulid  21571  mamurid  21572  mdetdiagid  21730  dscmet  23709  lgseisenlem2  26505  dchrisumlem3  26620  frgr2wwlk1  28672  poxp2  33769  poxp3  33775  bj-ssblem1  34814  bj-ssblem2  34815  bj-ax12  34817  bj-dtru  34978  wl-aleq  35673  wl-mo2df  35704  wl-eudf  35706  wl-euequf  35708  wl-mo2t  35709  dveeq2-o  36926  axc11n-16  36931  ax12eq  36934  ax12inda  36941  ax12v2-o  36942  fsuppind  40259  fphpd  40618  iotavalb  42001  disjinfi  42684  eusnsn  44471  fcoresf1  44514  2reu8i  44556  2reuimp0  44557  ichexmpl1  44873