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  2362  drsb1  2494  mo4  2560  sb8eulem  2592  cbvmovw  2596  cbvmow  2597  axextg  2704  reu6  3700  reu7  3706  reu8nf  3843  disjxun  5108  solin  5576  cbviotaw  6474  cbviota  6476  dff13f  7233  poxp  8110  poxp2  8125  poxp3  8132  unxpdomlem1  9204  unxpdomlem2  9205  aceq0  10078  zfac  10420  axrepndlem1  10552  zfcndac  10579  injresinj  13756  fsum2dlem  15743  ramub1lem2  17005  ramcl  17007  symgextf1  19358  mamulid  22335  mamurid  22336  mdetdiagid  22494  mdetunilem9  22514  alexsubALTlem3  23943  ptcmplem2  23947  dscmet  24467  dyadmbllem  25507  opnmbllem  25509  isppw2  27032  2sqreulem1  27364  2sqreunnlem1  27367  frgr2wwlk1  30265  disji2f  32513  disjif2  32517  cbvmodavw  36245  cbvsbdavw  36249  cbvsbdavw2  36250  bj-ssblem1  36649  bj-ssblem2  36650  cbveud  37367  wl-naevhba1v  37515  wl-equsb3  37551  mblfinlem1  37658  bfp  37825  dveeq1-o  38935  dveeq1-o16  38936  axc11n-16  38938  ax12eq  38941  aks6d1c6lem3  42167  aks6d1c7  42179  fsuppind  42585  eu6w  42671  fphpd  42811  ax6e2nd  44555  ax6e2ndVD  44904  ax6e2ndALT  44926  disjinfi  45193  iundjiun  46465  hspdifhsp  46621  hspmbl  46634  2reu8i  47118  2reuimp0  47119  ichexmpl1  47474  lcoss  48429