Theorem equequ1 2060

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 2051	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2056	. 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 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

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

This theorem is used by:  equvinv  2064  equvelv  2066  spaev  2089  sbjust  2100  equsb3  2142  cbvsbvf  2395  drsb1  2527  mo4  2594  sb8eulem  2626  cbvmovw  2630  cbvmow  2631  axextg  2737  reu6  3687  reu7  3693  reu8nf  3828  disjxun  5104  solin  5591  cbviotaw  6522  cbviota  6524  dff13f  7285  poxp  8170  poxp2  8190  poxp3  8197  unxpdomlem1  9278  unxpdomlem2  9279  aceq0  10227  zfac  10568  axrepndlem1  10707  zfcndac  10734  injresinj  13956  fsum2dlem  15968  ramub1lem2  17237  ramcl  17239  symgextf1  19668  mamulid  22789  mamurid  22790  mdetdiagid  22948  mdetunilem9  22968  alexsubALTlem3  24401  ptcmplem2  24405  dscmet  24924  dyadmbllem  25953  opnmbllem  25955  isppw2  27475  2sqreulem1  27806  2sqreunnlem1  27809  frgr2wwlk1  30963  disji2f  33246  disjif2  33250  reu6f  35792  elpssmo  36649  cbvmodavw  37230  cbvsbdavw  37234  cbvsbdavw2  37235  axtcond  37457  dfttc4  37509  bj-ssblem1  37744  bj-ssblem2  37745  cbveud  38500  wl-naevhba1v  38657  wl-equsb3  38693  mblfinlem1  38780  bfp  38961  dveeq1-o  40195  dveeq1-o16  40196  axc11n-16  40198  ax12eq  40201  aks6d1c6lem3  43425  aks6d1c7  43437  fsuppind  43822  eu6w  43891  fphpd  44027  ax6e2nd  45743  ax6e2ndVD  46092  ax6e2ndALT  46114  disjinfi  46422  iundjiun  47685  hspdifhsp  47841  hspmbl  47854  2reu8i  48399  2reuimp0  48400  ichexmpl1  48766  lcoss  49763