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

Theorem 3eqtr3a 2339
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)
Hypotheses
Ref Expression
3eqtr3a.1  |-  A  =  B
3eqtr3a.2  |-  ( ph  ->  A  =  C )
3eqtr3a.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3a
StepHypRef Expression
1 3eqtr3a.2 . 2  |-  ( ph  ->  A  =  C )
2 3eqtr3a.1 . . 3  |-  A  =  B
3 3eqtr3a.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3syl5eq 2327 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2317 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  uneqin  3420  coi2  5189  foima  5456  f1imacnv  5489  fvsnun2  5716  fnsnsplit  5717  phplem4  7043  php3  7047  rankopb  7524  fin4en1  7935  fpwwe2  8265  winacard  8314  mul02lem1  8988  cnegex2  8994  crreczi  11226  hashinf  11342  hashcard  11349  sqrneglem  11752  rlimresb  12039  sinhval  12434  coshval  12435  absefib  12478  efieq1re  12479  odngen  14888  restopnb  16906  cnmpt2t  17367  volsup2  18960  plypf1  19594  pige3  19885  sineq0  19889  eflog  19933  logef  19935  cxpsqr  20050  cubic2  20144  quart1  20152  asinsinlem  20187  asinsin  20188  2efiatan  20214  pclogsum  20454  lgsneg  20558  vc0  21125  vcm  21127  vcnegneg  21130  nvpi  21232  honegneg  22386  opsqrlem6  22725  sto1i  22816  mdexchi  22915  subfacp1lem1  23710  ghomfo  23998  rankaltopb  24513  bpoly4  24794  heiborlem6  26540  frlmup3  27252  trlcoat  30912  cdlemk54  31147
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator