Theorem equequ1 2026

Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)

Assertion

Ref	Expression
equequ1	⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))

Proof of Theorem equequ1

Step	Hyp	Ref	Expression
1		ax7 2017	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

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

This theorem is referenced by:  equvinv  2030  equvelv  2032  spaev  2055  sbjust  2066  equsb3  2106  cbvsbvf  2363  drsb1  2495  mo4  2561  sb8eulem  2593  cbvmovw  2597  cbvmow  2598  axextg  2705  reu6  3685  reu7  3691  reu8nf  3828  disjxun  5089  solin  5551  cbviotaw  6444  cbviota  6446  dff13f  7189  poxp  8058  poxp2  8073  poxp3  8080  unxpdomlem1  9140  unxpdomlem2  9141  aceq0  10006  zfac  10348  axrepndlem1  10480  zfcndac  10507  injresinj  13688  fsum2dlem  15674  ramub1lem2  16936  ramcl  16938  symgextf1  19331  mamulid  22354  mamurid  22355  mdetdiagid  22513  mdetunilem9  22533  alexsubALTlem3  23962  ptcmplem2  23966  dscmet  24485  dyadmbllem  25525  opnmbllem  25527  isppw2  27050  2sqreulem1  27382  2sqreunnlem1  27385  frgr2wwlk1  30304  disji2f  32552  disjif2  32556  cbvmodavw  36283  cbvsbdavw  36287  cbvsbdavw2  36288  bj-ssblem1  36687  bj-ssblem2  36688  cbveud  37405  wl-naevhba1v  37553  wl-equsb3  37589  mblfinlem1  37696  bfp  37863  dveeq1-o  38973  dveeq1-o16  38974  axc11n-16  38976  ax12eq  38979  aks6d1c6lem3  42204  aks6d1c7  42216  fsuppind  42622  eu6w  42708  fphpd  42848  ax6e2nd  44590  ax6e2ndVD  44939  ax6e2ndALT  44961  disjinfi  45228  iundjiun  46497  hspdifhsp  46653  hspmbl  46666  2reu8i  47143  2reuimp0  47144  ichexmpl1  47499  lcoss  48467