Theorem equequ2 2022

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 2018	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦))
2		equeuclr 2019	. 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 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004

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

This theorem is referenced by:  sbjust  2060  sbequ  2080  sb6  2082  equsb3r  2101  ax13lem2  2378  dveeq2ALT  2456  sb4b  2477  mojust  2536  mof  2560  eujust  2568  eujustALT  2569  eu6lem  2570  euf  2573  eleq1w  2821  mo2icl  3722  disjxun  5145  axrep2  5287  dtruALT2  5375  zfpair  5426  dtruOLD  5451  dfid3  5585  solin  5622  isso2i  5632  iotavalOLD  6536  dff13f  7275  dfwe2  7792  poxp2  8166  poxp3  8173  aceq0  10155  zfac  10497  axpowndlem4  10637  zfcndac  10656  injresinj  13823  infpn2  16946  ramub1lem2  17060  fullestrcsetc  18206  fullsetcestrc  18221  symgextf1  19453  mplcoe1  22072  evlslem2  22120  mamulid  22462  mamurid  22463  mdetdiagid  22621  dscmet  24600  lgseisenlem2  27434  dchrisumlem3  27549  frgr2wwlk1  30357  sbequbidv  36196  cbvsbdavw2  36237  bj-ssblem1  36636  bj-ssblem2  36637  bj-ax12  36639  wl-aleq  37515  wl-mo2df  37550  wl-eudf  37552  wl-euequf  37554  wl-mo2t  37555  dveeq2-o  38914  axc11n-16  38919  ax12eq  38922  ax12inda  38929  ax12v2-o  38930  aks6d1c6lem3  42153  fsuppind  42576  eu6w  42662  fphpd  42803  iotavalb  44425  disjinfi  45134  eusnsn  46975  fcoresf1  47018  2reu8i  47062  2reuimp0  47063  ichexmpl1  47393