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

Theorem equequ2 1739
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 1738 . 2
2 equcom 1734 . 2
3 equcom 1734 . 2
41, 2, 33bitr3g 287 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  ax12v  1795  ax12vOLD  1796  axc11nlem  1876  axc9lem1  1957  axc9lem2  2000  axc11nlemOLD  2008  dveeq2ALT  2042  ax12v2  2043  equvini  2047  sbequi  2076  dveeq2-o  2243  axc11n-16  2248  ax12eq  2251  ax12inda  2258  ax12v2-o  2259  eujust  2264  eujustALT  2265  euequ1  2268  euf  2272  eufOLD  2273  mo2  2274  moOLD  2314  2moOLDOLD  2371  2eu6OLD  2381  disjxun  4407  axrep2  4522  dtru  4600  zfpair  4646  dfid3  4754  isso2i  4790  iotaval  5511  dff13f  6098  dfwe2  6526  aceq0  8425  zfac  8766  axpowndlem4  8903  zfcndac  8923  injresinj  11784  infpn2  14132  ramub1lem2  14246  symgextf1  16085  mplcoe1  17721  evlslem2  17774  mamulid  18530  mamurid  18531  mdetdiagid  18674  dscmet  20564  lgseisenlem2  23089  dchrisumlem3  23140  usgrasscusgra  23860  wl-aleq  28824  wl-mo2dnae  28855  wl-mo2t  28856  fphpd  29615  iotavalb  30144  bj-axc11nlemv  33095  bj-axc15v  33110  bj-axrep2  33155  bj-dtru  33163  bj-eleq1w  33202
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730
This theorem depends on definitions:  df-bi 185  df-ex 1588
  Copyright terms: Public domain W3C validator