Theorem equequ1 2033

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788

This theorem is referenced by:  equvinv  2037  equvelv  2039  spaev  2058  sbjust  2069  equsb3  2105  sbievg  2362  drsb1  2498  mo4  2565  sb8eulem  2597  cbvmovw  2601  cbvmow  2602  axextg  2710  reu6  3639  reu7  3645  reu8nf  3789  disjxun  5051  solin  5493  cbviotaw  6345  cbviota  6348  dff13f  7068  poxp  7895  unxpdomlem1  8882  unxpdomlem2  8883  aceq0  9732  zfac  10074  axrepndlem1  10206  zfcndac  10233  injresinj  13363  fsum2dlem  15334  ramub1lem2  16580  ramcl  16582  symgextf1  18813  mamulid  21338  mamurid  21339  mdetdiagid  21497  mdetunilem9  21517  alexsubALTlem3  22946  ptcmplem2  22950  dscmet  23470  dyadmbllem  24496  opnmbllem  24498  isppw2  25997  2sqreulem1  26327  2sqreunnlem1  26330  frgr2wwlk1  28412  disji2f  30635  disjif2  30639  poxp2  33527  poxp3  33533  bj-ssblem1  34572  bj-ssblem2  34573  cbveud  35280  wl-naevhba1v  35416  wl-equsb3  35448  mblfinlem1  35551  bfp  35719  dveeq1-o  36686  dveeq1-o16  36687  axc11n-16  36689  ax12eq  36692  fsuppind  39989  mhphf  39995  fphpd  40341  ax6e2nd  41851  ax6e2ndVD  42201  ax6e2ndALT  42223  disjinfi  42404  iundjiun  43673  hspdifhsp  43829  hspmbl  43842  2reu8i  44277  2reuimp0  44278  ichexmpl1  44594  lcoss  45450