Theorem equequ1 2031

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

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780

This theorem is referenced by:  equvinv  2035  equvelv  2037  spaev  2056  sbjust  2067  equsb3  2108  drsb1  2534  mo4  2649  sb8eulem  2683  axextg  2798  reu6  3720  reu7  3726  reu8nf  3863  disjxun  5067  cbviotaw  6324  cbviota  6326  dff13f  7017  poxp  7825  unxpdomlem1  8725  unxpdomlem2  8726  aceq0  9547  zfac  9885  axrepndlem1  10017  zfcndac  10044  injresinj  13161  fsum2dlem  15128  ramub1lem2  16366  ramcl  16368  symgextf1  18552  mamulid  21053  mamurid  21054  mdetdiagid  21212  mdetunilem9  21232  alexsubALTlem3  22660  ptcmplem2  22664  dscmet  23185  dyadmbllem  24203  opnmbllem  24205  isppw2  25695  2sqreulem1  26025  2sqreunnlem1  26028  frgr2wwlk1  28111  disji2f  30330  disjif2  30334  bj-ssblem1  33991  bj-ssblem2  33992  cbveud  34657  wl-naevhba1v  34764  wl-equsb3  34796  mblfinlem1  34933  bfp  35106  dveeq1-o  36075  dveeq1-o16  36076  axc11n-16  36078  ax12eq  36081  fphpd  39419  ax6e2nd  40898  ax6e2ndVD  41248  ax6e2ndALT  41270  disjinfi  41460  iundjiun  42749  hspdifhsp  42905  hspmbl  42918  2reu8i  43319  2reuimp0  43320  ichexmpl1  43638  lcoss  44498