Theorem equequ1 2055

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 2046	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2051	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
3	1, 2	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  equvinv  2059  equvelv  2061  spaev  2084  sbjust  2095  equsb3  2138  cbvsbvf  2395  drsb1  2527  mo4  2594  sb8eulem  2626  cbvmovw  2630  cbvmow  2631  axextg  2737  reu6  3690  reu7  3696  reu8nf  3831  disjxun  5108  solin  5598  cbviotaw  6501  cbviota  6503  dff13f  7255  poxp  8125  poxp2  8140  poxp3  8147  unxpdomlem1  9217  unxpdomlem2  9218  aceq0  10103  zfac  10445  axrepndlem1  10578  zfcndac  10605  injresinj  13822  fsum2dlem  15823  ramub1lem2  17088  ramcl  17090  symgextf1  19492  mamulid  22579  mamurid  22580  mdetdiagid  22738  mdetunilem9  22758  alexsubALTlem3  24187  ptcmplem2  24191  dscmet  24710  dyadmbllem  25739  opnmbllem  25741  isppw2  27260  2sqreulem1  27591  2sqreunnlem1  27594  frgr2wwlk1  30661  disji2f  32903  disjif2  32907  cbvmodavw  36743  cbvsbdavw  36747  cbvsbdavw2  36748  axtcond  36970  dfttc4  37022  bj-ssblem1  37257  bj-ssblem2  37258  cbveud  37999  wl-naevhba1v  38156  wl-equsb3  38192  mblfinlem1  38289  bfp  38456  dveeq1-o  39690  dveeq1-o16  39691  axc11n-16  39693  ax12eq  39696  aks6d1c6lem3  42920  aks6d1c7  42932  fsuppind  43305  eu6w  43391  fphpd  43526  ax6e2nd  45250  ax6e2ndVD  45599  ax6e2ndALT  45621  disjinfi  45893  iundjiun  47157  hspdifhsp  47313  hspmbl  47326  2reu8i  47833  2reuimp0  47834  ichexmpl1  48201  lcoss  49199