Theorem equequ1 2024

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 2015	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2020	. 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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007

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

This theorem is referenced by:  equvinv  2028  equvelv  2030  spaev  2052  sbjust  2063  equsb3  2103  cbvsbvf  2369  drsb1  2503  mo4  2569  sb8eulem  2601  cbvmovw  2605  cbvmow  2606  axextg  2713  reu6  3748  reu7  3754  reu8nf  3899  disjxun  5164  solin  5634  cbviotaw  6532  cbviota  6535  dff13f  7293  poxp  8169  poxp2  8184  poxp3  8191  unxpdomlem1  9313  unxpdomlem2  9314  aceq0  10187  zfac  10529  axrepndlem1  10661  zfcndac  10688  injresinj  13838  fsum2dlem  15818  ramub1lem2  17074  ramcl  17076  symgextf1  19463  mamulid  22468  mamurid  22469  mdetdiagid  22627  mdetunilem9  22647  alexsubALTlem3  24078  ptcmplem2  24082  dscmet  24606  dyadmbllem  25653  opnmbllem  25655  isppw2  27176  2sqreulem1  27508  2sqreunnlem1  27511  frgr2wwlk1  30361  disji2f  32599  disjif2  32603  cbvmodavw  36216  cbvsbdavw  36220  cbvsbdavw2  36221  bj-ssblem1  36620  bj-ssblem2  36621  cbveud  37338  wl-naevhba1v  37474  wl-equsb3  37510  mblfinlem1  37617  bfp  37784  dveeq1-o  38891  dveeq1-o16  38892  axc11n-16  38894  ax12eq  38897  aks6d1c6lem3  42129  aks6d1c7  42141  fsuppind  42545  eu6w  42631  fphpd  42772  ax6e2nd  44529  ax6e2ndVD  44879  ax6e2ndALT  44901  disjinfi  45099  iundjiun  46381  hspdifhsp  46537  hspmbl  46550  2reu8i  47028  2reuimp0  47029  ichexmpl1  47343  lcoss  48165