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  7259  poxp  8140  poxp2  8160  poxp3  8167  unxpdomlem1  9248  unxpdomlem2  9249  aceq0  10198  zfac  10539  axrepndlem1  10678  zfcndac  10705  injresinj  13927  fsum2dlem  15937  ramub1lem2  17206  ramcl  17208  symgextf1  19636  mamulid  22757  mamurid  22758  mdetdiagid  22916  mdetunilem9  22936  alexsubALTlem3  24369  ptcmplem2  24373  dscmet  24892  dyadmbllem  25921  opnmbllem  25923  isppw2  27443  2sqreulem1  27774  2sqreunnlem1  27777  frgr2wwlk1  30931  disji2f  33214  disjif2  33218  cbvmodavw  37114  cbvsbdavw  37118  cbvsbdavw2  37119  axtcond  37341  dfttc4  37393  bj-ssblem1  37628  bj-ssblem2  37629  cbveud  38371  wl-naevhba1v  38528  wl-equsb3  38564  mblfinlem1  38651  bfp  38834  dveeq1-o  40068  dveeq1-o16  40069  axc11n-16  40071  ax12eq  40074  aks6d1c6lem3  43298  aks6d1c7  43310  fsuppind  43694  eu6w  43763  fphpd  43899  ax6e2nd  45617  ax6e2ndVD  45966  ax6e2ndALT  45988  disjinfi  46283  iundjiun  47546  hspdifhsp  47702  hspmbl  47715  2reu8i  48259  2reuimp0  48260  ichexmpl1  48627  lcoss  49624