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  2108  cbvsbvf  2365  drsb1  2497  mo4  2563  sb8eulem  2595  cbvmovw  2599  cbvmow  2600  axextg  2707  reu6  3681  reu7  3687  reu8nf  3824  disjxun  5091  solin  5554  cbviotaw  6449  cbviota  6451  dff13f  7195  poxp  8064  poxp2  8079  poxp3  8086  unxpdomlem1  9147  unxpdomlem2  9148  aceq0  10016  zfac  10358  axrepndlem1  10490  zfcndac  10517  injresinj  13693  fsum2dlem  15679  ramub1lem2  16941  ramcl  16943  symgextf1  19335  mamulid  22357  mamurid  22358  mdetdiagid  22516  mdetunilem9  22536  alexsubALTlem3  23965  ptcmplem2  23969  dscmet  24488  dyadmbllem  25528  opnmbllem  25530  isppw2  27053  2sqreulem1  27385  2sqreunnlem1  27388  frgr2wwlk1  30311  disji2f  32559  disjif2  32563  cbvmodavw  36315  cbvsbdavw  36319  cbvsbdavw2  36320  bj-ssblem1  36719  bj-ssblem2  36720  cbveud  37437  wl-naevhba1v  37585  wl-equsb3  37621  mblfinlem1  37717  bfp  37884  dveeq1-o  39054  dveeq1-o16  39055  axc11n-16  39057  ax12eq  39060  aks6d1c6lem3  42285  aks6d1c7  42297  fsuppind  42708  eu6w  42794  fphpd  42933  ax6e2nd  44675  ax6e2ndVD  45024  ax6e2ndALT  45046  disjinfi  45313  iundjiun  46582  hspdifhsp  46738  hspmbl  46751  2reu8i  47237  2reuimp0  47238  ichexmpl1  47593  lcoss  48561