Theorem equequ1 2048

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 2039	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧))
2		equtr 2044	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧))
3	1, 2	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧))

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803

This theorem is referenced by:  equvinv  2052  equvelv  2054  spaev  2077  rename-sb  2092  equsb3  2140  cbvsbvf  2397  drsb1  2529  mo4  2596  sb8eulem  2628  cbvmovw  2632  cbvmow  2633  axextg  2739  reu6  3692  reu7  3698  reu8nf  3833  disjxun  5103  solin  5587  cbviotaw  6488  cbviota  6490  dff13f  7243  poxp  8112  poxp2  8127  poxp3  8134  unxpdomlem1  9204  unxpdomlem2  9205  aceq0  10090  zfac  10432  axrepndlem1  10565  zfcndac  10592  injresinj  13811  fsum2dlem  15811  ramub1lem2  17077  ramcl  17079  symgextf1  19482  mamulid  22559  mamurid  22560  mdetdiagid  22718  mdetunilem9  22738  alexsubALTlem3  24167  ptcmplem2  24171  dscmet  24690  dyadmbllem  25719  opnmbllem  25721  isppw2  27237  2sqreulem1  27568  2sqreunnlem1  27571  frgr2wwlk1  30589  disji2f  32832  disjif2  32836  cbvmodavw  36623  cbvsbdavw  36627  cbvsbdavw2  36628  axtcond  36851  dfttc4  36903  bj-ssblem1  37138  bj-ssblem2  37139  cbveud  37878  wl-naevhba1v  38035  wl-equsb3  38071  mblfinlem1  38168  bfp  38335  dveeq1-o  39571  dveeq1-o16  39572  axc11n-16  39574  ax12eq  39577  aks6d1c6lem3  42801  aks6d1c7  42813  fsuppind  43184  eu6w  43270  fphpd  43405  ax6e2nd  45132  ax6e2ndVD  45481  ax6e2ndALT  45503  disjinfi  45768  iundjiun  47032  hspdifhsp  47188  hspmbl  47201  2reu8i  47705  2reuimp0  47706  ichexmpl1  48073  lcoss  49067