Theorem equequ2 2029

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 2025	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2026	. 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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  sbjust  2066  sbequ  2086  sb6  2088  equsb3r  2102  ax13lem2  2375  dveeq2ALT  2453  sb4b  2474  mojust  2533  mof  2557  eujust  2565  eujustALT  2566  eu6lem  2567  euf  2570  eleq1w  2816  mo2icl  3709  disjxun  5145  axrep2  5287  dtruALT2  5367  zfpair  5418  dtruOLD  5440  dfid3  5576  solin  5612  isso2i  5622  iotavalOLD  6514  dff13f  7251  dfwe2  7757  poxp2  8125  poxp3  8132  aceq0  10109  zfac  10451  axpowndlem4  10591  zfcndac  10610  injresinj  13749  infpn2  16842  ramub1lem2  16956  fullestrcsetc  18099  fullsetcestrc  18114  symgextf1  19283  mplcoe1  21583  evlslem2  21633  mamulid  21934  mamurid  21935  mdetdiagid  22093  dscmet  24072  lgseisenlem2  26868  dchrisumlem3  26983  frgr2wwlk1  29571  bj-ssblem1  35519  bj-ssblem2  35520  bj-ax12  35522  wl-aleq  36392  wl-mo2df  36423  wl-eudf  36425  wl-euequf  36427  wl-mo2t  36428  dveeq2-o  37791  axc11n-16  37796  ax12eq  37799  ax12inda  37806  ax12v2-o  37807  fsuppind  41159  fphpd  41539  iotavalb  43174  disjinfi  43876  eusnsn  45722  fcoresf1  45765  2reu8i  45807  2reuimp0  45808  ichexmpl1  46123