Theorem equequ1 2026

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

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  equvinv  2030  equvelv  2032  spaev  2055  sbjust  2066  equsb3  2108  cbvsbvf  2367  drsb1  2499  mo4  2566  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  axextg  2710  reu6  3684  reu7  3690  reu8nf  3827  disjxun  5096  solin  5559  cbviotaw  6455  cbviota  6457  dff13f  7201  poxp  8070  poxp2  8085  poxp3  8092  unxpdomlem1  9156  unxpdomlem2  9157  aceq0  10028  zfac  10370  axrepndlem1  10503  zfcndac  10530  injresinj  13707  fsum2dlem  15693  ramub1lem2  16955  ramcl  16957  symgextf1  19350  mamulid  22385  mamurid  22386  mdetdiagid  22544  mdetunilem9  22564  alexsubALTlem3  23993  ptcmplem2  23997  dscmet  24516  dyadmbllem  25556  opnmbllem  25558  isppw2  27081  2sqreulem1  27413  2sqreunnlem1  27416  frgr2wwlk1  30404  disji2f  32652  disjif2  32656  cbvmodavw  36444  cbvsbdavw  36448  cbvsbdavw2  36449  bj-ssblem1  36855  bj-ssblem2  36856  cbveud  37573  wl-naevhba1v  37721  wl-equsb3  37757  mblfinlem1  37854  bfp  38021  dveeq1-o  39191  dveeq1-o16  39192  axc11n-16  39194  ax12eq  39197  aks6d1c6lem3  42422  aks6d1c7  42434  fsuppind  42829  eu6w  42915  fphpd  43054  ax6e2nd  44795  ax6e2ndVD  45144  ax6e2ndALT  45166  disjinfi  45432  iundjiun  46700  hspdifhsp  46856  hspmbl  46869  2reu8i  47355  2reuimp0  47356  ichexmpl1  47711  lcoss  48678