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

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

Proof of Theorem equequ2
StepHypRef Expression
1 equequ1 1798 . 2
2 equcom 1794 . 2
3 equcom 1794 . 2
41, 2, 33bitr3g 287 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  ax12v  1855  ax12vOLD  1856  axc11nlem  1938  axc9lem1  2001  axc9lem2  2040  axc11nlemOLD  2048  dveeq2ALT  2082  ax12v2  2083  equvini  2087  sbequi  2116  dveeq2-o  2263  axc11n-16  2268  ax12eq  2271  ax12inda  2278  ax12v2-o  2279  eujust  2284  eujustALT  2285  euequ1  2288  euf  2292  mo2  2293  2eu6OLD  2384  disjxun  4450  axrep2  4565  dtru  4643  zfpair  4689  dfid3  4801  isso2i  4837  iotaval  5567  dff13f  6167  dfwe2  6617  aceq0  8520  zfac  8861  axpowndlem4  8998  zfcndac  9018  injresinj  11926  infpn2  14431  ramub1lem2  14545  symgextf1  16446  mplcoe1  18127  evlslem2  18180  mamulid  18943  mamurid  18944  mdetdiagid  19102  dscmet  21093  lgseisenlem2  23625  dchrisumlem3  23676  usgrasscusgra  24483  wl-aleq  29988  wl-mo2dnae  30019  wl-mo2t  30020  fphpd  30750  iotavalb  31337  fullestrcsetc  32657  fullsetcestrc  32672  bj-axc11nlemv  34315  bj-axc15v  34330  bj-axrep2  34375  bj-dtru  34383  bj-eleq1w  34422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator