Theorem equequ1 2025

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 2016	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2021	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008

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

This theorem is referenced by:  equvinv  2029  equvelv  2031  spaev  2053  sbjust  2064  equsb3  2104  cbvsbvf  2361  drsb1  2493  mo4  2559  sb8eulem  2591  cbvmovw  2595  cbvmow  2596  axextg  2703  reu6  3697  reu7  3703  reu8nf  3840  disjxun  5105  solin  5573  cbviotaw  6471  cbviota  6473  dff13f  7230  poxp  8107  poxp2  8122  poxp3  8129  unxpdomlem1  9197  unxpdomlem2  9198  aceq0  10071  zfac  10413  axrepndlem1  10545  zfcndac  10572  injresinj  13749  fsum2dlem  15736  ramub1lem2  16998  ramcl  17000  symgextf1  19351  mamulid  22328  mamurid  22329  mdetdiagid  22487  mdetunilem9  22507  alexsubALTlem3  23936  ptcmplem2  23940  dscmet  24460  dyadmbllem  25500  opnmbllem  25502  isppw2  27025  2sqreulem1  27357  2sqreunnlem1  27360  frgr2wwlk1  30258  disji2f  32506  disjif2  32510  cbvmodavw  36238  cbvsbdavw  36242  cbvsbdavw2  36243  bj-ssblem1  36642  bj-ssblem2  36643  cbveud  37360  wl-naevhba1v  37508  wl-equsb3  37544  mblfinlem1  37651  bfp  37818  dveeq1-o  38928  dveeq1-o16  38929  axc11n-16  38931  ax12eq  38934  aks6d1c6lem3  42160  aks6d1c7  42172  fsuppind  42578  eu6w  42664  fphpd  42804  ax6e2nd  44548  ax6e2ndVD  44897  ax6e2ndALT  44919  disjinfi  45186  iundjiun  46458  hspdifhsp  46614  hspmbl  46627  2reu8i  47114  2reuimp0  47115  ichexmpl1  47470  lcoss  48425