Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  equequ1 Structured version   Visualization version   GIF version

Theorem equequ1 1939
 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
StepHypRef Expression
1 ax7 1930 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 1935 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 201 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696 This theorem is referenced by:  equequ2OLD  1942  spaev  1965  drsb1  2365  equsb3lem  2419  sb8eu  2491  axext3ALT  2593  reu6  3362  reu7  3368  disjxun  4581  cbviota  5773  dff13f  6417  poxp  7176  unxpdomlem1  8049  unxpdomlem2  8050  aceq0  8824  zfac  9165  axrepndlem1  9293  zfcndac  9320  injresinj  12451  fsum2dlem  14343  ramub1lem2  15569  ramcl  15571  symgextf1  17664  mamulid  20066  mamurid  20067  mdetdiagid  20225  mdetunilem9  20245  alexsubALTlem3  21663  ptcmplem2  21667  dscmet  22187  dyadmbllem  23173  opnmbllem  23175  isppw2  24641  frg2wot1  26584  disji2f  28772  disjif2  28776  bj-ssblem1  31819  bj-ssblem2  31820  bj-axext3  31957  wl-naevhba1v  32483  wl-equsb3  32516  mblfinlem1  32616  bfp  32793  dveeq1-o  33238  dveeq1-o16  33239  axc11n-16  33241  ax12eq  33244  fphpd  36398  ax6e2nd  37795  ax6e2ndVD  38166  ax6e2ndALT  38188  disjinfi  38375  iundjiun  39353  hspdifhsp  39506  hspmbl  39519  frgr2wwlk1  41494  lcoss  42019
 Copyright terms: Public domain W3C validator