Theorem equequ1 2029

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  equvinv  2033  equvelv  2035  spaev  2056  sbjust  2067  equsb3  2103  sbievg  2361  drsb1  2499  mo4  2566  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  axextg  2711  reu6  3656  reu7  3662  reu8nf  3806  disjxun  5068  solin  5519  cbviotaw  6383  cbviota  6386  dff13f  7110  poxp  7940  unxpdomlem1  8956  unxpdomlem2  8957  aceq0  9805  zfac  10147  axrepndlem1  10279  zfcndac  10306  injresinj  13436  fsum2dlem  15410  ramub1lem2  16656  ramcl  16658  symgextf1  18944  mamulid  21498  mamurid  21499  mdetdiagid  21657  mdetunilem9  21677  alexsubALTlem3  23108  ptcmplem2  23112  dscmet  23634  dyadmbllem  24668  opnmbllem  24670  isppw2  26169  2sqreulem1  26499  2sqreunnlem1  26502  frgr2wwlk1  28594  disji2f  30817  disjif2  30821  poxp2  33717  poxp3  33723  bj-ssblem1  34762  bj-ssblem2  34763  cbveud  35470  wl-naevhba1v  35606  wl-equsb3  35638  mblfinlem1  35741  bfp  35909  dveeq1-o  36876  dveeq1-o16  36877  axc11n-16  36879  ax12eq  36882  fsuppind  40202  mhphf  40208  fphpd  40554  ax6e2nd  42067  ax6e2ndVD  42417  ax6e2ndALT  42439  disjinfi  42620  iundjiun  43888  hspdifhsp  44044  hspmbl  44057  2reu8i  44492  2reuimp0  44493  ichexmpl1  44809  lcoss  45665