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  2394  drsb1  2526  mo4  2593  sb8eulem  2625  cbvmovw  2629  cbvmow  2630  axextg  2736  reu6  3687  reu7  3693  reu8nf  3827  disjxun  5105  solin  5594  cbviotaw  6500  cbviota  6502  dff13f  7256  poxp  8130  poxp2  8145  poxp3  8152  unxpdomlem1  9230  unxpdomlem2  9231  aceq0  10125  zfac  10466  axrepndlem1  10605  zfcndac  10632  injresinj  13851  fsum2dlem  15860  ramub1lem2  17125  ramcl  17127  symgextf1  19554  mamulid  22669  mamurid  22670  mdetdiagid  22828  mdetunilem9  22848  alexsubALTlem3  24281  ptcmplem2  24285  dscmet  24804  dyadmbllem  25833  opnmbllem  25835  isppw2  27359  2sqreulem1  27690  2sqreunnlem1  27693  frgr2wwlk1  30817  disji2f  33058  disjif2  33062  cbvmodavw  36878  cbvsbdavw  36882  cbvsbdavw2  36883  axtcond  37105  dfttc4  37157  bj-ssblem1  37392  bj-ssblem2  37393  cbveud  38134  wl-naevhba1v  38291  wl-equsb3  38327  mblfinlem1  38414  bfp  38582  dveeq1-o  39816  dveeq1-o16  39817  axc11n-16  39819  ax12eq  39822  aks6d1c6lem3  43046  aks6d1c7  43058  fsuppind  43444  eu6w  43530  fphpd  43665  ax6e2nd  45389  ax6e2ndVD  45738  ax6e2ndALT  45760  disjinfi  46032  iundjiun  47296  hspdifhsp  47452  hspmbl  47465  2reu8i  48009  2reuimp0  48010  ichexmpl1  48377  lcoss  49374