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  7254  poxp  8113  poxp2  8128  poxp3  8135  unxpdomlem1  9249  unxpdomlem2  9250  aceq0  10112  zfac  10454  axrepndlem1  10586  zfcndac  10613  injresinj  13752  fsum2dlem  15715  ramub1lem2  16959  ramcl  16961  symgextf1  19288  mamulid  21942  mamurid  21943  mdetdiagid  22101  mdetunilem9  22121  alexsubALTlem3  23552  ptcmplem2  23556  dscmet  24080  dyadmbllem  25115  opnmbllem  25117  isppw2  26616  2sqreulem1  26946  2sqreunnlem1  26949  frgr2wwlk1  29579  disji2f  31803  disjif2  31807  bj-ssblem1  35526  bj-ssblem2  35527  cbveud  36248  wl-naevhba1v  36384  wl-equsb3  36416  mblfinlem1  36520  bfp  36687  dveeq1-o  37800  dveeq1-o16  37801  axc11n-16  37803  ax12eq  37806  fsuppind  41164  fphpd  41544  ax6e2nd  43309  ax6e2ndVD  43659  ax6e2ndALT  43681  disjinfi  43881  iundjiun  45166  hspdifhsp  45322  hspmbl  45335  2reu8i  45811  2reuimp0  45812  ichexmpl1  46127  lcoss  47107