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  3673  reu7  3679  reu8nf  3816  disjxun  5084  solin  5557  cbviotaw  6453  cbviota  6455  dff13f  7201  poxp  8069  poxp2  8084  poxp3  8091  unxpdomlem1  9157  unxpdomlem2  9158  aceq0  10029  zfac  10371  axrepndlem1  10504  zfcndac  10531  injresinj  13708  fsum2dlem  15694  ramub1lem2  16956  ramcl  16958  symgextf1  19354  mamulid  22384  mamurid  22385  mdetdiagid  22543  mdetunilem9  22563  alexsubALTlem3  23992  ptcmplem2  23996  dscmet  24515  dyadmbllem  25544  opnmbllem  25546  isppw2  27065  2sqreulem1  27397  2sqreunnlem1  27400  frgr2wwlk1  30388  disji2f  32636  disjif2  32640  cbvmodavw  36438  cbvsbdavw  36442  cbvsbdavw2  36443  axtcond  36666  dfttc4  36718  bj-ssblem1  36946  bj-ssblem2  36947  cbveud  37684  wl-naevhba1v  37836  wl-equsb3  37872  mblfinlem1  37969  bfp  38136  dveeq1-o  39372  dveeq1-o16  39373  axc11n-16  39375  ax12eq  39378  aks6d1c6lem3  42603  aks6d1c7  42615  fsuppind  43022  eu6w  43108  fphpd  43247  ax6e2nd  44988  ax6e2ndVD  45337  ax6e2ndALT  45359  disjinfi  45625  iundjiun  46892  hspdifhsp  47048  hspmbl  47061  2reu8i  47547  2reuimp0  47548  ichexmpl1  47903  lcoss  48870