Theorem equequ1 2028

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  equvinv  2032  equvelv  2034  spaev  2055  sbjust  2066  equsb3  2101  sbievg  2361  drsb1  2499  mo4  2566  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  axextg  2711  reu6  3661  reu7  3667  reu8nf  3810  disjxun  5072  solin  5528  cbviotaw  6398  cbviota  6401  dff13f  7129  poxp  7969  unxpdomlem1  9027  unxpdomlem2  9028  aceq0  9874  zfac  10216  axrepndlem1  10348  zfcndac  10375  injresinj  13508  fsum2dlem  15482  ramub1lem2  16728  ramcl  16730  symgextf1  19029  mamulid  21590  mamurid  21591  mdetdiagid  21749  mdetunilem9  21769  alexsubALTlem3  23200  ptcmplem2  23204  dscmet  23728  dyadmbllem  24763  opnmbllem  24765  isppw2  26264  2sqreulem1  26594  2sqreunnlem1  26597  frgr2wwlk1  28693  disji2f  30916  disjif2  30920  poxp2  33790  poxp3  33796  bj-ssblem1  34835  bj-ssblem2  34836  cbveud  35543  wl-naevhba1v  35679  wl-equsb3  35711  mblfinlem1  35814  bfp  35982  dveeq1-o  36949  dveeq1-o16  36950  axc11n-16  36952  ax12eq  36955  fsuppind  40279  mhphf  40285  fphpd  40638  ax6e2nd  42178  ax6e2ndVD  42528  ax6e2ndALT  42550  disjinfi  42731  iundjiun  43998  hspdifhsp  44154  hspmbl  44167  2reu8i  44605  2reuimp0  44606  ichexmpl1  44921  lcoss  45777