Theorem equequ1 2027

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 2018	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2023	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  equvinv  2031  equvelv  2033  spaev  2056  sbjust  2067  equsb3  2109  cbvsbvf  2368  drsb1  2500  mo4  2567  sb8eulem  2599  cbvmovw  2603  cbvmow  2604  axextg  2711  reu6  3673  reu7  3679  reu8nf  3816  disjxun  5084  solin  5559  cbviotaw  6455  cbviota  6457  dff13f  7203  poxp  8071  poxp2  8086  poxp3  8093  unxpdomlem1  9159  unxpdomlem2  9160  aceq0  10031  zfac  10373  axrepndlem1  10506  zfcndac  10533  injresinj  13737  fsum2dlem  15723  ramub1lem2  16989  ramcl  16991  symgextf1  19387  mamulid  22416  mamurid  22417  mdetdiagid  22575  mdetunilem9  22595  alexsubALTlem3  24024  ptcmplem2  24028  dscmet  24547  dyadmbllem  25576  opnmbllem  25578  isppw2  27092  2sqreulem1  27423  2sqreunnlem1  27426  frgr2wwlk1  30414  disji2f  32662  disjif2  32666  cbvmodavw  36448  cbvsbdavw  36452  cbvsbdavw2  36453  axtcond  36676  dfttc4  36728  bj-ssblem1  36964  bj-ssblem2  36965  cbveud  37702  wl-naevhba1v  37859  wl-equsb3  37895  mblfinlem1  37992  bfp  38159  dveeq1-o  39395  dveeq1-o16  39396  axc11n-16  39398  ax12eq  39401  aks6d1c6lem3  42625  aks6d1c7  42637  fsuppind  43037  eu6w  43123  fphpd  43262  ax6e2nd  45003  ax6e2ndVD  45352  ax6e2ndALT  45374  disjinfi  45640  iundjiun  46906  hspdifhsp  47062  hspmbl  47075  2reu8i  47573  2reuimp0  47574  ichexmpl1  47941  lcoss  48924