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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011

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

This theorem is referenced by:  equvinv  2032  equvelv  2034  spaev  2055  sbjust  2066  equsb3  2101  cbvsbvf  2360  drsb1  2494  mo4  2560  sb8eulem  2592  cbvmovw  2596  cbvmow  2597  axextg  2705  reu6  3722  reu7  3728  reu8nf  3871  disjxun  5146  solin  5613  cbviotaw  6502  cbviota  6505  dff13f  7257  poxp  8116  poxp2  8131  poxp3  8138  unxpdomlem1  9252  unxpdomlem2  9253  aceq0  10115  zfac  10457  axrepndlem1  10589  zfcndac  10616  injresinj  13757  fsum2dlem  15720  ramub1lem2  16964  ramcl  16966  symgextf1  19330  mamulid  22163  mamurid  22164  mdetdiagid  22322  mdetunilem9  22342  alexsubALTlem3  23773  ptcmplem2  23777  dscmet  24301  dyadmbllem  25340  opnmbllem  25342  isppw2  26843  2sqreulem1  27173  2sqreunnlem1  27176  frgr2wwlk1  29837  disji2f  32063  disjif2  32067  bj-ssblem1  35834  bj-ssblem2  35835  cbveud  36556  wl-naevhba1v  36692  wl-equsb3  36724  mblfinlem1  36828  bfp  36995  dveeq1-o  38108  dveeq1-o16  38109  axc11n-16  38111  ax12eq  38114  fsuppind  41464  fphpd  41856  ax6e2nd  43621  ax6e2ndVD  43971  ax6e2ndALT  43993  disjinfi  44190  iundjiun  45475  hspdifhsp  45631  hspmbl  45644  2reu8i  46120  2reuimp0  46121  ichexmpl1  46436  lcoss  47205