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  3688  reu7  3694  reu8nf  3831  disjxun  5093  solin  5558  cbviotaw  6449  cbviota  6451  dff13f  7196  poxp  8068  poxp2  8083  poxp3  8090  unxpdomlem1  9155  unxpdomlem2  9156  aceq0  10031  zfac  10373  axrepndlem1  10505  zfcndac  10532  injresinj  13709  fsum2dlem  15695  ramub1lem2  16957  ramcl  16959  symgextf1  19318  mamulid  22344  mamurid  22345  mdetdiagid  22503  mdetunilem9  22523  alexsubALTlem3  23952  ptcmplem2  23956  dscmet  24476  dyadmbllem  25516  opnmbllem  25518  isppw2  27041  2sqreulem1  27373  2sqreunnlem1  27376  frgr2wwlk1  30291  disji2f  32539  disjif2  32543  cbvmodavw  36223  cbvsbdavw  36227  cbvsbdavw2  36228  bj-ssblem1  36627  bj-ssblem2  36628  cbveud  37345  wl-naevhba1v  37493  wl-equsb3  37529  mblfinlem1  37636  bfp  37803  dveeq1-o  38913  dveeq1-o16  38914  axc11n-16  38916  ax12eq  38919  aks6d1c6lem3  42145  aks6d1c7  42157  fsuppind  42563  eu6w  42649  fphpd  42789  ax6e2nd  44532  ax6e2ndVD  44881  ax6e2ndALT  44903  disjinfi  45170  iundjiun  46442  hspdifhsp  46598  hspmbl  46611  2reu8i  47098  2reuimp0  47099  ichexmpl1  47454  lcoss  48422