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  2141  cbvsbvf  2398  drsb1  2530  mo4  2597  sb8eulem  2629  cbvmovw  2633  cbvmow  2634  axextg  2740  reu6  3692  reu7  3698  reu8nf  3833  disjxun  5112  solin  5601  cbviotaw  6506  cbviota  6508  dff13f  7260  poxp  8133  poxp2  8148  poxp3  8155  unxpdomlem1  9226  unxpdomlem2  9227  aceq0  10121  zfac  10462  axrepndlem1  10595  zfcndac  10622  injresinj  13839  fsum2dlem  15847  ramub1lem2  17112  ramcl  17114  symgextf1  19522  mamulid  22635  mamurid  22636  mdetdiagid  22794  mdetunilem9  22814  alexsubALTlem3  24243  ptcmplem2  24247  dscmet  24766  dyadmbllem  25795  opnmbllem  25797  isppw2  27316  2sqreulem1  27647  2sqreunnlem1  27650  frgr2wwlk1  30717  disji2f  32959  disjif2  32963  cbvmodavw  36803  cbvsbdavw  36807  cbvsbdavw2  36808  axtcond  37030  dfttc4  37082  bj-ssblem1  37317  bj-ssblem2  37318  cbveud  38059  wl-naevhba1v  38216  wl-equsb3  38252  mblfinlem1  38349  bfp  38516  dveeq1-o  39750  dveeq1-o16  39751  axc11n-16  39753  ax12eq  39756  aks6d1c6lem3  42980  aks6d1c7  42992  fsuppind  43363  eu6w  43449  fphpd  43584  ax6e2nd  45308  ax6e2ndVD  45657  ax6e2ndALT  45679  disjinfi  45951  iundjiun  47215  hspdifhsp  47371  hspmbl  47384  2reu8i  47891  2reuimp0  47892  ichexmpl1  48259  lcoss  49257