Theorem equequ1 2023

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 2014	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2019	. 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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006

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

This theorem is referenced by:  equvinv  2027  equvelv  2029  spaev  2051  sbjust  2062  equsb3  2102  cbvsbvf  2365  drsb1  2499  mo4  2565  sb8eulem  2597  cbvmovw  2601  cbvmow  2602  axextg  2709  reu6  3731  reu7  3737  reu8nf  3876  disjxun  5140  solin  5618  cbviotaw  6520  cbviota  6522  dff13f  7277  poxp  8154  poxp2  8169  poxp3  8176  unxpdomlem1  9287  unxpdomlem2  9288  aceq0  10159  zfac  10501  axrepndlem1  10633  zfcndac  10660  injresinj  13828  fsum2dlem  15807  ramub1lem2  17066  ramcl  17068  symgextf1  19440  mamulid  22448  mamurid  22449  mdetdiagid  22607  mdetunilem9  22627  alexsubALTlem3  24058  ptcmplem2  24062  dscmet  24586  dyadmbllem  25635  opnmbllem  25637  isppw2  27159  2sqreulem1  27491  2sqreunnlem1  27494  frgr2wwlk1  30349  disji2f  32591  disjif2  32595  cbvmodavw  36252  cbvsbdavw  36256  cbvsbdavw2  36257  bj-ssblem1  36656  bj-ssblem2  36657  cbveud  37374  wl-naevhba1v  37522  wl-equsb3  37558  mblfinlem1  37665  bfp  37832  dveeq1-o  38937  dveeq1-o16  38938  axc11n-16  38940  ax12eq  38943  aks6d1c6lem3  42174  aks6d1c7  42186  fsuppind  42605  eu6w  42691  fphpd  42832  ax6e2nd  44583  ax6e2ndVD  44933  ax6e2ndALT  44955  disjinfi  45202  iundjiun  46480  hspdifhsp  46636  hspmbl  46649  2reu8i  47130  2reuimp0  47131  ichexmpl1  47461  lcoss  48358