Theorem equequ1 2032

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 2023	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2028	. 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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015

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

This theorem is referenced by:  equvinv  2036  equvelv  2038  spaev  2061  sbjust  2072  equsb3  2114  cbvsbvf  2371  drsb1  2503  mo4  2570  sb8eulem  2602  cbvmovw  2606  cbvmow  2607  axextg  2714  reu6  3674  reu7  3680  reu8nf  3816  disjxun  5077  solin  5560  cbviotaw  6455  cbviota  6457  dff13f  7206  poxp  8075  poxp2  8090  poxp3  8097  unxpdomlem1  9163  unxpdomlem2  9164  aceq0  10038  zfac  10380  axrepndlem1  10513  zfcndac  10540  injresinj  13744  fsum2dlem  15730  ramub1lem2  16996  ramcl  16998  symgextf1  19394  mamulid  22431  mamurid  22432  mdetdiagid  22590  mdetunilem9  22610  alexsubALTlem3  24039  ptcmplem2  24043  dscmet  24562  dyadmbllem  25591  opnmbllem  25593  isppw2  27103  2sqreulem1  27434  2sqreunnlem1  27437  frgr2wwlk1  30424  disji2f  32673  disjif2  32677  cbvmodavw  36485  cbvsbdavw  36489  cbvsbdavw2  36490  axtcond  36713  dfttc4  36765  bj-ssblem1  37001  bj-ssblem2  37002  cbveud  37741  wl-naevhba1v  37898  wl-equsb3  37934  mblfinlem1  38031  bfp  38198  dveeq1-o  39434  dveeq1-o16  39435  axc11n-16  39437  ax12eq  39440  aks6d1c6lem3  42664  aks6d1c7  42676  fsuppind  43047  eu6w  43133  fphpd  43268  ax6e2nd  45009  ax6e2ndVD  45358  ax6e2ndALT  45380  disjinfi  45646  iundjiun  46910  hspdifhsp  47066  hspmbl  47079  2reu8i  47583  2reuimp0  47584  ichexmpl1  47951  lcoss  48934