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

Theorem equequ2 1952
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 1948 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
2 equeuclr 1949 . 2 (𝑥 = 𝑦 → (𝑧 = 𝑦𝑧 = 𝑥))
31, 2impbid 202 1 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704
This theorem is referenced by:  axc11nlemOLD2  1987  ax12vOLDOLD  2050  axc11nlemOLD  2159  ax13lem2  2295  axc15  2302  axc11nlemALT  2305  dveeq2ALT  2339  ax12v2OLD  2341  eujust  2471  eujustALT  2472  euequ1  2475  euf  2477  mo2  2478  eleq1w  2683  disjxun  4649  axrep2  4771  dtru  4855  zfpair  4902  dfid3  5023  isso2i  5065  iotaval  5860  dff13f  6510  dfwe2  6978  aceq0  8938  zfac  9279  axpowndlem4  9419  zfcndac  9438  injresinj  12584  infpn2  15611  ramub1lem2  15725  fullestrcsetc  16785  fullsetcestrc  16800  symgextf1  17835  mplcoe1  19459  evlslem2  19506  mamulid  20241  mamurid  20242  mdetdiagid  20400  dscmet  22371  lgseisenlem2  25095  dchrisumlem3  25174  frgr2wwlk1  27180  bj-ssbjust  32602  bj-ssbequ  32613  bj-ssblem1  32614  bj-ssblem2  32615  bj-ssb1a  32616  bj-ssb1  32617  bj-ssbcom3lem  32634  bj-axrep2  32773  bj-dtru  32781  bj-ax8  32871  wl-aleq  33302  wl-mo2df  33332  wl-eudf  33334  wl-euequ1f  33336  wl-mo2t  33337  dveeq2-o  34044  axc11n-16  34049  ax12eq  34052  ax12inda  34059  ax12v2-o  34060  fphpd  37206  iotavalb  38457  disjinfi  39202
  Copyright terms: Public domain W3C validator