Theorem equequ1 2044

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

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  equvinv  2048  equvelv  2050  spaev  2073  rename-sb  2088  equsb3  2136  cbvsbvf  2393  drsb1  2525  mo4  2592  sb8eulem  2624  cbvmovw  2628  cbvmow  2629  axextg  2735  reu6  3688  reu7  3694  reu8nf  3830  disjxun  5097  solin  5580  cbviotaw  6480  cbviota  6482  dff13f  7235  poxp  8103  poxp2  8118  poxp3  8125  unxpdomlem1  9196  unxpdomlem2  9197  aceq0  10071  zfac  10414  axrepndlem1  10547  zfcndac  10574  injresinj  13794  fsum2dlem  15780  ramub1lem2  17046  ramcl  17048  symgextf1  19444  mamulid  22481  mamurid  22482  mdetdiagid  22640  mdetunilem9  22660  alexsubALTlem3  24089  ptcmplem2  24093  dscmet  24612  dyadmbllem  25641  opnmbllem  25643  isppw2  27156  2sqreulem1  27487  2sqreunnlem1  27490  frgr2wwlk1  30477  disji2f  32726  disjif2  32730  cbvmodavw  36574  cbvsbdavw  36578  cbvsbdavw2  36579  axtcond  36802  dfttc4  36854  bj-ssblem1  37090  bj-ssblem2  37091  cbveud  37830  wl-naevhba1v  37987  wl-equsb3  38023  mblfinlem1  38120  bfp  38287  dveeq1-o  39523  dveeq1-o16  39524  axc11n-16  39526  ax12eq  39529  aks6d1c6lem3  42753  aks6d1c7  42765  fsuppind  43136  eu6w  43222  fphpd  43357  ax6e2nd  45098  ax6e2ndVD  45447  ax6e2ndALT  45469  disjinfi  45734  iundjiun  46998  hspdifhsp  47154  hspmbl  47167  2reu8i  47671  2reuimp0  47672  ichexmpl1  48039  lcoss  49022