Theorem equequ1 2058

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 2049	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2054	. 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 1943  ax-6 2000  ax-7 2041

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

This theorem is used by:  equvinv  2062  equvelv  2064  spaev  2087  sbjust  2098  equsb3  2140  cbvsbvf  2393  drsb1  2525  mo4  2592  sb8eulem  2624  cbvmovw  2628  cbvmow  2629  axextg  2735  reu6  3684  reu7  3690  reu8nf  3824  disjxun  5101  solin  5586  cbviotaw  6494  cbviota  6496  dff13f  7251  poxp  8129  poxp2  8144  poxp3  8151  unxpdomlem1  9231  unxpdomlem2  9232  aceq0  10178  zfac  10519  axrepndlem1  10658  zfcndac  10685  injresinj  13906  fsum2dlem  15916  ramub1lem2  17185  ramcl  17187  symgextf1  19615  mamulid  22736  mamurid  22737  mdetdiagid  22895  mdetunilem9  22915  alexsubALTlem3  24348  ptcmplem2  24352  dscmet  24871  dyadmbllem  25900  opnmbllem  25902  isppw2  27424  2sqreulem1  27755  2sqreunnlem1  27758  frgr2wwlk1  30912  disji2f  33153  disjif2  33157  cbvmodavw  37009  cbvsbdavw  37013  cbvsbdavw2  37014  axtcond  37236  dfttc4  37288  bj-ssblem1  37523  bj-ssblem2  37524  cbveud  38263  wl-naevhba1v  38420  wl-equsb3  38456  mblfinlem1  38543  bfp  38726  dveeq1-o  39960  dveeq1-o16  39961  axc11n-16  39963  ax12eq  39966  aks6d1c6lem3  43190  aks6d1c7  43202  fsuppind  43580  eu6w  43641  fphpd  43776  ax6e2nd  45500  ax6e2ndVD  45849  ax6e2ndALT  45871  disjinfi  46150  iundjiun  47414  hspdifhsp  47570  hspmbl  47583  2reu8i  48127  2reuimp0  48128  ichexmpl1  48495  lcoss  49492