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  2366  drsb1  2500  mo4  2566  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  axextg  2710  reu6  3714  reu7  3720  reu8nf  3857  disjxun  5122  solin  5593  cbviotaw  6496  cbviota  6498  dff13f  7253  poxp  8132  poxp2  8147  poxp3  8154  unxpdomlem1  9263  unxpdomlem2  9264  aceq0  10137  zfac  10479  axrepndlem1  10611  zfcndac  10638  injresinj  13809  fsum2dlem  15791  ramub1lem2  17052  ramcl  17054  symgextf1  19407  mamulid  22384  mamurid  22385  mdetdiagid  22543  mdetunilem9  22563  alexsubALTlem3  23992  ptcmplem2  23996  dscmet  24516  dyadmbllem  25557  opnmbllem  25559  isppw2  27082  2sqreulem1  27414  2sqreunnlem1  27417  frgr2wwlk1  30315  disji2f  32563  disjif2  32567  cbvmodavw  36273  cbvsbdavw  36277  cbvsbdavw2  36278  bj-ssblem1  36677  bj-ssblem2  36678  cbveud  37395  wl-naevhba1v  37543  wl-equsb3  37579  mblfinlem1  37686  bfp  37853  dveeq1-o  38958  dveeq1-o16  38959  axc11n-16  38961  ax12eq  38964  aks6d1c6lem3  42190  aks6d1c7  42202  fsuppind  42588  eu6w  42674  fphpd  42814  ax6e2nd  44558  ax6e2ndVD  44907  ax6e2ndALT  44929  disjinfi  45196  iundjiun  46469  hspdifhsp  46625  hspmbl  46638  2reu8i  47122  2reuimp0  47123  ichexmpl1  47463  lcoss  48392