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 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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  sbjust  2068  sbequ  2088  sb6  2090  equsb3r  2107  ax13lem2  2383  dveeq2ALT  2465  sb4b  2488  sb4bOLD  2489  mojust  2597  mof  2622  eujust  2631  eujustALT  2632  eu6lem  2633  euf  2636  eleq1w  2872  disjxun  5028  axrep2  5157  dtru  5236  zfpair  5287  dfid3  5427  isso2i  5472  iotaval  6298  dff13f  6992  dfwe2  7476  aceq0  9529  zfac  9871  axpowndlem4  10011  zfcndac  10030  injresinj  13153  infpn2  16239  ramub1lem2  16353  fullestrcsetc  17393  fullsetcestrc  17408  symgextf1  18541  mplcoe1  20705  evlslem2  20751  mamulid  21046  mamurid  21047  mdetdiagid  21205  dscmet  23179  lgseisenlem2  25960  dchrisumlem3  26075  frgr2wwlk1  28114  bj-ssblem1  34100  bj-ssblem2  34101  bj-ax12  34103  bj-dtru  34254  wl-aleq  34940  wl-mo2df  34971  wl-eudf  34973  wl-euequf  34975  wl-mo2t  34976  dveeq2-o  36229  axc11n-16  36234  ax12eq  36237  ax12inda  36244  ax12v2-o  36245  fsuppind  39456  fphpd  39757  iotavalb  41134  disjinfi  41820  eusnsn  43618  2reu8i  43669  2reuimp0  43670  ichexmpl1  43986