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

Theorem equequ1 1938
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 1929 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 1934 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 200 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  equequ2OLD  1941  spaev  1964  drsb1  2364  equsb3lem  2418  sb8eu  2490  axext3ALT  2592  reu6  3361  reu7  3367  disjxun  4575  cbviota  5759  dff13f  6395  poxp  7154  unxpdomlem1  8027  unxpdomlem2  8028  aceq0  8802  zfac  9143  axrepndlem1  9271  zfcndac  9298  injresinj  12409  fsum2dlem  14292  ramub1lem2  15518  ramcl  15520  symgextf1  17613  mamulid  20014  mamurid  20015  mdetdiagid  20173  mdetunilem9  20193  alexsubALTlem3  21611  ptcmplem2  21615  dscmet  22135  dyadmbllem  23118  opnmbllem  23120  isppw2  24586  frg2wot1  26378  disji2f  28606  disjif2  28610  bj-ssblem1  31653  bj-ssblem2  31654  bj-axext3  31791  wl-naevhba1v  32307  wl-equsb3  32340  mblfinlem1  32440  bfp  32617  dveeq1-o  33062  dveeq1-o16  33063  axc11n-16  33065  ax12eq  33068  fphpd  36222  ax6e2nd  37619  ax6e2ndVD  37990  ax6e2ndALT  38012  disjinfi  38199  iundjiun  39177  hspdifhsp  39330  hspmbl  39343  frgr2wwlk1  41516  lcoss  42041
  Copyright terms: Public domain W3C validator