Theorem equequ2 2045

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 2041	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2042	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥))
3	1, 2	impbid 214	1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  rename-sb  2088  sbequ  2115  sb6  2117  equsb3r  2137  ax13lem2  2406  dveeq2ALT  2484  sb4b  2505  mojust  2564  mof  2589  eujust  2597  eujustALT  2598  eu6lem  2599  euf  2602  eleq1w  2844  mo2icl  3675  disjxun  5095  axrep2  5227  dtruALT2  5324  zfpair  5375  dfid3  5541  solin  5578  isso2i  5588  dff13f  7234  dfwe2  7752  poxp2  8117  poxp3  8124  aceq0  10068  zfac  10411  axpowndlem4  10552  zfcndac  10571  injresinj  13791  infpn2  16940  ramub1lem2  17054  fullestrcsetc  18174  fullsetcestrc  18189  symgextf1  19452  mplcoe1  22078  evlslem2  22120  mamulid  22489  mamurid  22490  mdetdiagid  22648  dscmet  24620  lgseisenlem2  27428  dchrisumlem3  27543  frgr2wwlk1  30488  sbequbidv  36535  cbvsbdavw2  36576  axtcond  36799  dfttc4  36851  mh-setindnd  36858  bj-ssblem1  37087  bj-ssblem2  37088  bj-ax12  37090  wl-aleq  37999  wl-mo2df  38034  wl-eudf  38036  wl-euequf  38038  wl-mo2t  38039  dveeq2-o  39518  axc11n-16  39523  ax12eq  39526  ax12inda  39533  ax12v2-o  39534  aks6d1c6lem3  42750  fsuppind  43133  eu6w  43219  fphpd  43354  iotavalb  44967  disjinfi  45731  eusnsn  47581  fcoresf1  47624  2reu8i  47668  2reuimp0  47669  ichexmpl1  48036  nprmmul3  48096