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

Theorem equequ2 2034
Description: An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.)
Assertion
Ref Expression
equequ2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))

Proof of Theorem equequ2
StepHypRef Expression
1 equtrr 2030 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equeuclr 2031 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑦𝑧 = 𝑥))
31, 2impbid 215 1 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782
This theorem is referenced by:  sbjust  2069  sbequ  2091  sb6  2094  equsb3r  2111  ax13lem2  2396  dveeq2ALT  2478  sb4b  2501  sb4bOLD  2502  mojust  2623  mof  2648  eujust  2657  eujustALT  2658  eu6lem  2659  euf  2662  eleq1w  2898  disjxun  5050  axrep2  5179  dtru  5258  zfpair  5309  dfid3  5449  isso2i  5495  iotaval  6317  dff13f  7006  dfwe2  7490  aceq0  9542  zfac  9880  axpowndlem4  10020  zfcndac  10039  injresinj  13162  infpn2  16247  ramub1lem2  16361  fullestrcsetc  17401  fullsetcestrc  17416  symgextf1  18549  mplcoe1  20712  evlslem2  20758  mamulid  21053  mamurid  21054  mdetdiagid  21212  dscmet  23185  lgseisenlem2  25966  dchrisumlem3  26081  frgr2wwlk1  28120  bj-ssblem1  34047  bj-ssblem2  34048  bj-ax12  34050  bj-dtru  34201  wl-aleq  34888  wl-mo2df  34919  wl-eudf  34921  wl-euequf  34923  wl-mo2t  34924  dveeq2-o  36177  axc11n-16  36182  ax12eq  36185  ax12inda  36192  ax12v2-o  36193  fsuppind  39393  fphpd  39677  iotavalb  41058  disjinfi  41749  eusnsn  43548  2reu8i  43599  2reuimp0  43600  ichexmpl1  43916
  Copyright terms: Public domain W3C validator