Theorem equequ1 2057

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  equvinv  2061  equvelv  2063  spaev  2086  sbjust  2097  equsb3  2139  cbvsbvf  2392  drsb1  2524  mo4  2591  sb8eulem  2623  cbvmovw  2627  cbvmow  2628  axextg  2734  reu6  3683  reu7  3689  reu8nf  3823  disjxun  5100  solin  5585  cbviotaw  6501  cbviota  6503  dff13f  7260  poxp  8143  poxp2  8163  poxp3  8170  unxpdomlem1  9251  unxpdomlem2  9252  aceq0  10201  zfac  10542  axrepndlem1  10681  zfcndac  10708  injresinj  13930  fsum2dlem  15942  ramub1lem2  17211  ramcl  17213  symgextf1  19641  mamulid  22762  mamurid  22763  mdetdiagid  22921  mdetunilem9  22941  alexsubALTlem3  24374  ptcmplem2  24378  dscmet  24897  dyadmbllem  25926  opnmbllem  25928  isppw2  27448  2sqreulem1  27779  2sqreunnlem1  27782  frgr2wwlk1  30936  disji2f  33219  disjif2  33223  reu6f  35756  cbvmodavw  37132  cbvsbdavw  37136  cbvsbdavw2  37137  axtcond  37359  dfttc4  37411  bj-ssblem1  37646  bj-ssblem2  37647  cbveud  38389  wl-naevhba1v  38546  wl-equsb3  38582  mblfinlem1  38669  bfp  38852  dveeq1-o  40086  dveeq1-o16  40087  axc11n-16  40089  ax12eq  40092  aks6d1c6lem3  43316  aks6d1c7  43328  fsuppind  43712  eu6w  43781  fphpd  43917  ax6e2nd  45635  ax6e2ndVD  45984  ax6e2ndALT  46006  disjinfi  46301  iundjiun  47564  hspdifhsp  47720  hspmbl  47733  2reu8i  48277  2reuimp0  48278  ichexmpl1  48645  lcoss  49642