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

Theorem equequ1 2122
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 2113 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
2 equtr 2118 . 2 (𝑥 = 𝑦 → (𝑦 = 𝑧𝑥 = 𝑧))
31, 2impbid 203 1 (𝑥 = 𝑦 → (𝑥 = 𝑧𝑦 = 𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875
This theorem is referenced by:  equvinv  2127  equvelv  2130  spaev  2145  drsb1  2468  equsb3lem  2523  sb8eu  2624  axext3ALT  2746  reu6  3554  reu7  3560  reu8nf  3674  disjxun  4807  cbviota  6036  dff13f  6705  poxp  7491  unxpdomlem1  8371  unxpdomlem2  8372  aceq0  9192  zfac  9535  axrepndlem1  9667  zfcndac  9694  injresinj  12797  fsum2dlem  14788  ramub1lem2  16012  ramcl  16014  symgextf1  18106  mamulid  20523  mamurid  20524  mdetdiagid  20683  mdetunilem9  20703  alexsubALTlem3  22132  ptcmplem2  22136  dscmet  22656  dyadmbllem  23657  opnmbllem  23659  isppw2  25132  frgr2wwlk1  27567  disji2f  29773  disjif2  29777  bj-ssbjust  32987  bj-ssblem1  32999  bj-ssblem2  33000  bj-axext3  33131  wl-naevhba1v  33663  wl-equsb3  33695  mblfinlem1  33802  bfp  33977  dveeq1-o  34823  dveeq1-o16  34824  axc11n-16  34826  ax12eq  34829  fphpd  37990  ax6e2nd  39368  ax6e2ndVD  39728  ax6e2ndALT  39750  disjinfi  39959  iundjiun  41246  hspdifhsp  41402  hspmbl  41415  lcoss  42826
  Copyright terms: Public domain W3C validator