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

Theorem 3eqtr3a 2498
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 2486 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2476 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  uneqin  3577  coi2  5415  foima  5687  f1imacnv  5720  fvsnun2  5958  fnsnsplit  5959  phplem4  7318  php3  7322  rankopb  7807  fin4en1  8220  fpwwe2  8549  winacard  8598  mul02lem1  9273  cnegex2  9279  crreczi  11535  hashinf  11654  hashcard  11669  sqrneglem  12103  rlimresb  12390  sinhval  12786  coshval  12787  absefib  12830  efieq1re  12831  sadcaddlem  13000  sadaddlem  13009  odngen  15242  restopnb  17270  cnmpt2t  17736  volsup2  19528  plypf1  20162  pige3  20456  sineq0  20460  eflog  20505  logef  20507  cxpsqr  20625  cubic2  20719  quart1  20727  asinsinlem  20762  asinsin  20763  2efiatan  20789  pclogsum  21030  lgsneg  21134  vc0  22079  vcm  22081  vcnegneg  22084  nvpi  22186  honegneg  23340  opsqrlem6  23679  sto1i  23770  mdexchi  23869  cnre2csqlem  24339  subfacp1lem1  24896  ghomfo  25133  rankaltopb  25855  bpoly3  26135  bpoly4  26136  dvtan  26293  heiborlem6  26563  frlmup3  27267  dvsinexp  27754  stirlinglem1  27837  trlcoat  31618  cdlemk54  31853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2435
  Copyright terms: Public domain W3C validator