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 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011

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

This theorem is referenced by:  sbjust  2066  sbequ  2086  sb6  2088  equsb3r  2102  ax13lem2  2376  dveeq2ALT  2454  sb4b  2475  sb4bOLD  2476  mojust  2539  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  eleq1w  2821  mo2icl  3649  disjxun  5072  axrep2  5212  dtruALT2  5293  zfpair  5344  dtru  5359  dfid3  5492  solin  5528  isso2i  5538  iotaval  6407  dff13f  7129  dfwe2  7624  aceq0  9874  zfac  10216  axpowndlem4  10356  zfcndac  10375  injresinj  13508  infpn2  16614  ramub1lem2  16728  fullestrcsetc  17868  fullsetcestrc  17883  symgextf1  19029  mplcoe1  21238  evlslem2  21289  mamulid  21590  mamurid  21591  mdetdiagid  21749  dscmet  23728  lgseisenlem2  26524  dchrisumlem3  26639  frgr2wwlk1  28693  poxp2  33790  poxp3  33796  bj-ssblem1  34835  bj-ssblem2  34836  bj-ax12  34838  bj-dtru  34999  wl-aleq  35694  wl-mo2df  35725  wl-eudf  35727  wl-euequf  35729  wl-mo2t  35730  dveeq2-o  36947  axc11n-16  36952  ax12eq  36955  ax12inda  36962  ax12v2-o  36963  fsuppind  40279  fphpd  40638  iotavalb  42048  disjinfi  42731  eusnsn  44520  fcoresf1  44563  2reu8i  44605  2reuimp0  44606  ichexmpl1  44921