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

Theorem equequ2 1698
 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 1696 . 2
2 equcom 1692 . 2
3 equcom 1692 . 2
41, 2, 33bitr3g 279 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177 This theorem is referenced by:  a9e  1952  ax10lem2  2023  ax10lem2OLD  2026  dveeq2OLD  2029  ax10lem4OLD  2030  ax9OLD  2033  dveeq2  2073  ax11v2  2074  ax11v2OLD  2075  sbequi  2136  ax11vALT  2172  dveeq2-o  2260  dveeq2-o16  2261  ax10-16  2266  ax11eq  2269  ax11inda  2276  ax11v2-o  2277  eujust  2282  eujustALT  2283  euf  2286  mo  2302  2mo  2358  2eu6  2365  disjxun  4202  axrep2  4314  dtru  4382  zfpair  4393  dfid3  4491  isso2i  4527  dfwe2  4754  iotaval  5421  dff13f  5998  aceq0  7989  zfac  8330  axpowndlem4  8465  zfcndac  8484  injresinj  11190  infpn2  13271  ramub1lem2  13385  mplcoe1  16518  evlslem2  16558  dscmet  18610  lgseisenlem2  21124  dchrisumlem3  21175  usgrasscusgra  21482  wl-aleq  26200  fphpd  26831  mamulid  27390  mamurid  27391  iotavalb  27562  dveeq2NEW7  29364  ax9NEW7  29369  ax10lem4NEW7  29372  ax11v2NEW7  29431 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687 This theorem depends on definitions:  df-bi 178  df-ex 1551
 Copyright terms: Public domain W3C validator