Theorem equequ1 2048

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 2039	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2044	. 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 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

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

This theorem is referenced by:  equvinv  2052  equvelv  2054  spaev  2077  rename-sb  2092  equsb3  2140  cbvsbvf  2397  drsb1  2529  mo4  2596  sb8eulem  2628  cbvmovw  2632  cbvmow  2633  axextg  2739  reu6  3692  reu7  3698  reu8nf  3833  disjxun  5102  solin  5586  cbviotaw  6488  cbviota  6490  dff13f  7243  poxp  8112  poxp2  8127  poxp3  8134  unxpdomlem1  9204  unxpdomlem2  9205  aceq0  10090  zfac  10432  axrepndlem1  10565  zfcndac  10592  injresinj  13808  fsum2dlem  15809  ramub1lem2  17075  ramcl  17077  symgextf1  19479  mamulid  22555  mamurid  22556  mdetdiagid  22714  mdetunilem9  22734  alexsubALTlem3  24163  ptcmplem2  24167  dscmet  24686  dyadmbllem  25715  opnmbllem  25717  isppw2  27233  2sqreulem1  27564  2sqreunnlem1  27567  frgr2wwlk1  30585  disji2f  32828  disjif2  32832  cbvmodavw  36618  cbvsbdavw  36622  cbvsbdavw2  36623  axtcond  36846  dfttc4  36898  bj-ssblem1  37133  bj-ssblem2  37134  cbveud  37873  wl-naevhba1v  38030  wl-equsb3  38066  mblfinlem1  38163  bfp  38330  dveeq1-o  39566  dveeq1-o16  39567  axc11n-16  39569  ax12eq  39572  aks6d1c6lem3  42796  aks6d1c7  42808  fsuppind  43179  eu6w  43265  fphpd  43400  ax6e2nd  45126  ax6e2ndVD  45475  ax6e2ndALT  45497  disjinfi  45769  iundjiun  47033  hspdifhsp  47189  hspmbl  47202  2reu8i  47706  2reuimp0  47707  ichexmpl1  48074  lcoss  49068