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

Theorem 3eqtr3a 2352
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 2340 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2330 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  uneqin  3433  coi2  5205  foima  5472  f1imacnv  5505  fvsnun2  5732  fnsnsplit  5733  phplem4  7059  php3  7063  rankopb  7540  fin4en1  7951  fpwwe2  8281  winacard  8330  mul02lem1  9004  cnegex2  9010  crreczi  11242  hashinf  11358  hashcard  11365  sqrneglem  11768  rlimresb  12055  sinhval  12450  coshval  12451  absefib  12494  efieq1re  12495  odngen  14904  restopnb  16922  cnmpt2t  17383  volsup2  18976  plypf1  19610  pige3  19901  sineq0  19905  eflog  19949  logef  19951  cxpsqr  20066  cubic2  20160  quart1  20168  asinsinlem  20203  asinsin  20204  2efiatan  20230  pclogsum  20470  lgsneg  20574  vc0  21141  vcm  21143  vcnegneg  21146  nvpi  21248  honegneg  22402  opsqrlem6  22741  sto1i  22832  mdexchi  22931  subfacp1lem1  23725  ghomfo  24013  rankaltopb  24585  bpoly4  24866  heiborlem6  26643  frlmup3  27355  trlcoat  31534  cdlemk54  31769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator