Theorem equequ1 2027

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 2018	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2023	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

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

This theorem is referenced by:  equvinv  2031  equvelv  2033  spaev  2056  sbjust  2067  equsb3  2109  cbvsbvf  2368  drsb1  2500  mo4  2567  sb8eulem  2599  cbvmovw  2603  cbvmow  2604  axextg  2711  reu6  3686  reu7  3692  reu8nf  3829  disjxun  5098  solin  5567  cbviotaw  6463  cbviota  6465  dff13f  7211  poxp  8080  poxp2  8095  poxp3  8102  unxpdomlem1  9168  unxpdomlem2  9169  aceq0  10040  zfac  10382  axrepndlem1  10515  zfcndac  10542  injresinj  13719  fsum2dlem  15705  ramub1lem2  16967  ramcl  16969  symgextf1  19362  mamulid  22397  mamurid  22398  mdetdiagid  22556  mdetunilem9  22576  alexsubALTlem3  24005  ptcmplem2  24009  dscmet  24528  dyadmbllem  25568  opnmbllem  25570  isppw2  27093  2sqreulem1  27425  2sqreunnlem1  27428  frgr2wwlk1  30416  disji2f  32663  disjif2  32667  cbvmodavw  36463  cbvsbdavw  36467  cbvsbdavw2  36468  bj-ssblem1  36893  bj-ssblem2  36894  cbveud  37621  wl-naevhba1v  37769  wl-equsb3  37805  mblfinlem1  37902  bfp  38069  dveeq1-o  39305  dveeq1-o16  39306  axc11n-16  39308  ax12eq  39311  aks6d1c6lem3  42536  aks6d1c7  42548  fsuppind  42942  eu6w  43028  fphpd  43167  ax6e2nd  44908  ax6e2ndVD  45257  ax6e2ndALT  45279  disjinfi  45545  iundjiun  46812  hspdifhsp  46968  hspmbl  46981  2reu8i  47467  2reuimp0  47468  ichexmpl1  47823  lcoss  48790