Theorem equequ1 2021

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 2012	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2017	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
3	1, 2	impbid 212	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776

This theorem is referenced by:  equvinv  2025  equvelv  2027  spaev  2049  sbjust  2060  equsb3  2100  cbvsbvf  2363  drsb1  2497  mo4  2563  sb8eulem  2595  cbvmovw  2599  cbvmow  2600  axextg  2707  reu6  3734  reu7  3740  reu8nf  3885  disjxun  5145  solin  5622  cbviotaw  6522  cbviota  6524  dff13f  7275  poxp  8151  poxp2  8166  poxp3  8173  unxpdomlem1  9283  unxpdomlem2  9284  aceq0  10155  zfac  10497  axrepndlem1  10629  zfcndac  10656  injresinj  13823  fsum2dlem  15802  ramub1lem2  17060  ramcl  17062  symgextf1  19453  mamulid  22462  mamurid  22463  mdetdiagid  22621  mdetunilem9  22641  alexsubALTlem3  24072  ptcmplem2  24076  dscmet  24600  dyadmbllem  25647  opnmbllem  25649  isppw2  27172  2sqreulem1  27504  2sqreunnlem1  27507  frgr2wwlk1  30357  disji2f  32596  disjif2  32600  cbvmodavw  36232  cbvsbdavw  36236  cbvsbdavw2  36237  bj-ssblem1  36636  bj-ssblem2  36637  cbveud  37354  wl-naevhba1v  37500  wl-equsb3  37536  mblfinlem1  37643  bfp  37810  dveeq1-o  38916  dveeq1-o16  38917  axc11n-16  38919  ax12eq  38922  aks6d1c6lem3  42153  aks6d1c7  42165  fsuppind  42576  eu6w  42662  fphpd  42803  ax6e2nd  44555  ax6e2ndVD  44905  ax6e2ndALT  44927  disjinfi  45134  iundjiun  46415  hspdifhsp  46571  hspmbl  46584  2reu8i  47062  2reuimp0  47063  ichexmpl1  47393  lcoss  48281