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  2367  drsb1  2499  mo4  2566  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  axextg  2710  reu6  3672  reu7  3678  reu8nf  3815  disjxun  5083  solin  5566  cbviotaw  6461  cbviota  6463  dff13f  7210  poxp  8078  poxp2  8093  poxp3  8100  unxpdomlem1  9166  unxpdomlem2  9167  aceq0  10040  zfac  10382  axrepndlem1  10515  zfcndac  10542  injresinj  13746  fsum2dlem  15732  ramub1lem2  16998  ramcl  17000  symgextf1  19396  mamulid  22406  mamurid  22407  mdetdiagid  22565  mdetunilem9  22585  alexsubALTlem3  24014  ptcmplem2  24018  dscmet  24537  dyadmbllem  25566  opnmbllem  25568  isppw2  27078  2sqreulem1  27409  2sqreunnlem1  27412  frgr2wwlk1  30399  disji2f  32647  disjif2  32651  cbvmodavw  36432  cbvsbdavw  36436  cbvsbdavw2  36437  axtcond  36660  dfttc4  36712  bj-ssblem1  36948  bj-ssblem2  36949  cbveud  37688  wl-naevhba1v  37845  wl-equsb3  37881  mblfinlem1  37978  bfp  38145  dveeq1-o  39381  dveeq1-o16  39382  axc11n-16  39384  ax12eq  39387  aks6d1c6lem3  42611  aks6d1c7  42623  fsuppind  43023  eu6w  43109  fphpd  43244  ax6e2nd  44985  ax6e2ndVD  45334  ax6e2ndALT  45356  disjinfi  45622  iundjiun  46888  hspdifhsp  47044  hspmbl  47057  2reu8i  47561  2reuimp0  47562  ichexmpl1  47929  lcoss  48912