Theorem equequ2 2030

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 2026	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2027	. 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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

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

This theorem is referenced by:  sbjust  2067  sbequ  2087  sb6  2089  equsb3r  2104  ax13lem2  2376  dveeq2ALT  2454  sb4b  2475  sb4bOLD  2476  mojust  2539  mof  2563  eujust  2571  eujustALT  2572  eu6lem  2573  euf  2576  eleq1w  2821  mo2icl  3644  disjxun  5068  axrep2  5208  dtru  5288  zfpair  5339  dfid3  5483  solin  5519  isso2i  5529  iotaval  6392  dff13f  7110  dfwe2  7602  aceq0  9805  zfac  10147  axpowndlem4  10287  zfcndac  10306  injresinj  13436  infpn2  16542  ramub1lem2  16656  fullestrcsetc  17784  fullsetcestrc  17799  symgextf1  18944  mplcoe1  21148  evlslem2  21199  mamulid  21498  mamurid  21499  mdetdiagid  21657  dscmet  23634  lgseisenlem2  26429  dchrisumlem3  26544  frgr2wwlk1  28594  poxp2  33717  poxp3  33723  bj-ssblem1  34762  bj-ssblem2  34763  bj-ax12  34765  bj-dtru  34926  wl-aleq  35621  wl-mo2df  35652  wl-eudf  35654  wl-euequf  35656  wl-mo2t  35657  dveeq2-o  36874  axc11n-16  36879  ax12eq  36882  ax12inda  36889  ax12v2-o  36890  fsuppind  40202  fphpd  40554  iotavalb  41937  disjinfi  42620  eusnsn  44407  fcoresf1  44450  2reu8i  44492  2reuimp0  44493  ichexmpl1  44809