Theorem equequ1 2009

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

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762

This theorem is referenced by:  equvinv  2013  equvelv  2015  spaev  2028  sbjust  2041  equsb3  2076  drsb1  2489  mo4  2607  sb8eulem  2650  axextg  2771  reu6  3654  reu7  3660  reu8nf  3792  disjxun  4964  cbviota  6199  dff13f  6884  poxp  7680  unxpdomlem1  8573  unxpdomlem2  8574  aceq0  9395  zfac  9733  axrepndlem1  9865  zfcndac  9892  injresinj  13013  fsum2dlem  14963  ramub1lem2  16197  ramcl  16199  symgextf1  18285  mamulid  20739  mamurid  20740  mdetdiagid  20898  mdetunilem9  20918  alexsubALTlem3  22346  ptcmplem2  22350  dscmet  22870  dyadmbllem  23888  opnmbllem  23890  isppw2  25379  2sqreulem1  25709  2sqreunnlem1  25712  frgr2wwlk1  27805  disji2f  30022  disjif2  30026  bj-ssblem1  33595  bj-ssblem2  33596  cbveud  34209  wl-naevhba1v  34318  wl-equsb3  34348  mblfinlem1  34485  bfp  34659  dveeq1-o  35627  dveeq1-o16  35628  axc11n-16  35630  ax12eq  35633  fphpd  38923  ax6e2nd  40456  ax6e2ndVD  40806  ax6e2ndALT  40828  disjinfi  41019  iundjiun  42310  hspdifhsp  42466  hspmbl  42479  2reu8i  42854  2reuimp0  42855  ichexmpl1  43139  lcoss  43997