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

Theorem equequ2 1730
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.)
Assertion
Ref Expression
equequ2

Proof of Theorem equequ2
StepHypRef Expression
1 equequ1 1729 . 2
2 equcom 1725 . 2
3 equcom 1725 . 2
41, 2, 33bitr3g 281 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178
This theorem is referenced by:  axc9lem1  1936  axc9lem2  1979  axc11nlem  1987  dveeq2ALT  2023  ax12v2  2024  equvini  2028  sbequi  2055  ax12vALT  2123  dveeq2-o  2225  axc11n-16  2230  ax12eq  2233  ax12inda  2240  ax12v2-o  2241  eujust  2246  eujustALT  2247  euf  2251  eufOLD  2252  mo2  2253  moOLD  2289  2mo  2344  2moOLD  2345  2eu6  2352  disjxun  4265  axrep2  4380  dtru  4455  zfpair  4501  dfid3  4608  isso2i  4644  iotaval  5364  dff13f  5941  dfwe2  6363  aceq0  8235  zfac  8576  axpowndlem4  8713  zfcndac  8732  injresinj  11580  infpn2  13914  ramub1lem2  14028  symgextf1  15863  mplcoe1  17351  evlslem2  17392  mamulid  18002  mamurid  18003  dscmet  19865  lgseisenlem2  22430  dchrisumlem3  22481  usgrasscusgra  23070  wl-aleq  28061  wl-ax12v2  28081  fphpd  28828  iotavalb  29357  bj-axc11nlemv  31756  bj-axc15v  31771  bj-axrep2  31804  bj-dtru  31812  bj-eleq1w  31838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721
This theorem depends on definitions:  df-bi 179  df-ex 1582
  Copyright terms: Public domain W3C validator