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

Theorem 3eqtr3a 2545
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
Hypotheses
Ref Expression
3eqtr3a.1
3eqtr3a.2
3eqtr3a.3
Assertion
Ref Expression
3eqtr3a

Proof of Theorem 3eqtr3a
StepHypRef Expression
1 3eqtr3a.2 . 2
2 3eqtr3a.1 . . 3
3 3eqtr3a.3 . . 3
42, 3syl5eq 2533 . 2
51, 4eqtr3d 2523 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  =wceq 1670
This theorem is referenced by:  uneqin  3637  coi2  5374  foima  5642  f1imacnv  5674  fvsnun2  5929  fnsnsplit  5930  phplem4  7454  php3  7458  rankopb  7945  fin4en1  8360  fpwwe2  8689  winacard  8738  mul02lem1  9422  cnegex2  9428  crreczi  11838  hashinf  11957  hashcard  11974  cshw0  12278  cshwn  12281  sqrneglem  12603  rlimresb  12890  sinhval  13285  coshval  13286  absefib  13329  efieq1re  13330  sadcaddlem  13500  sadaddlem  13509  odngen  15820  frlmup3  17746  mat0op  17790  restopnb  18253  cnmpt2t  18720  volsup2  20512  plypf1  21146  pige3  21445  sineq0  21449  eflog  21494  logef  21496  cxpsqr  21614  cubic2  21709  quart1  21717  asinsinlem  21752  asinsin  21753  2efiatan  21779  pclogsum  22020  lgsneg  22124  vc0  23069  vcm  23071  vcnegneg  23074  nvpi  23176  honegneg  24332  opsqrlem6  24671  sto1i  24762  mdexchi  24861  cnre2csqlem  25519  subfacp1lem1  26213  ghomfo  26450  rankaltopb  27163  bpoly3  27443  bpoly4  27444  dvtan  27622  dvcncxp1  27657  dvasin  27660  heiborlem6  27897  dvsinexp  28965  stirlinglem1  29048  numclwlk1lem2fo  29869  trlcoat  33070  cdlemk54  33305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-12 1768  ax-ext 2470
This theorem depends on definitions:  df-bi 179  df-ex 1566  df-cleq 2482
  Copyright terms: Public domain W3C validator