Theorem equequ2 2025

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

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778

This theorem is referenced by:  sbjust  2063  sbequ  2083  sb6  2085  equsb3r  2104  ax13lem2  2384  dveeq2ALT  2462  sb4b  2483  mojust  2542  mof  2566  eujust  2574  eujustALT  2575  eu6lem  2576  euf  2579  eleq1w  2827  mo2icl  3736  disjxun  5164  axrep2  5306  dtruALT2  5388  zfpair  5439  dtruOLD  5461  dfid3  5596  solin  5634  isso2i  5644  iotavalOLD  6547  dff13f  7293  dfwe2  7809  poxp2  8184  poxp3  8191  aceq0  10187  zfac  10529  axpowndlem4  10669  zfcndac  10688  injresinj  13838  infpn2  16960  ramub1lem2  17074  fullestrcsetc  18220  fullsetcestrc  18235  symgextf1  19463  mplcoe1  22078  evlslem2  22126  mamulid  22468  mamurid  22469  mdetdiagid  22627  dscmet  24606  lgseisenlem2  27438  dchrisumlem3  27553  frgr2wwlk1  30361  sbequbidv  36180  cbvsbdavw2  36221  bj-ssblem1  36620  bj-ssblem2  36621  bj-ax12  36623  wl-aleq  37489  wl-mo2df  37524  wl-eudf  37526  wl-euequf  37528  wl-mo2t  37529  dveeq2-o  38889  axc11n-16  38894  ax12eq  38897  ax12inda  38904  ax12v2-o  38905  aks6d1c6lem3  42129  fsuppind  42545  eu6w  42631  fphpd  42772  iotavalb  44399  disjinfi  45099  eusnsn  46941  fcoresf1  46984  2reu8i  47028  2reuimp0  47029  ichexmpl1  47343