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

Theorem 3eqtr3a 2494
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 2482 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2472 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  uneqin  3594  coi2  5388  foima  5660  f1imacnv  5693  fvsnun2  5931  fnsnsplit  5932  phplem4  7291  php3  7295  rankopb  7780  fin4en1  8191  fpwwe2  8520  winacard  8569  mul02lem1  9244  cnegex2  9250  crreczi  11506  hashinf  11625  hashcard  11640  sqrneglem  12074  rlimresb  12361  sinhval  12757  coshval  12758  absefib  12801  efieq1re  12802  sadcaddlem  12971  sadaddlem  12980  odngen  15213  restopnb  17241  cnmpt2t  17707  volsup2  19499  plypf1  20133  pige3  20427  sineq0  20431  eflog  20476  logef  20478  cxpsqr  20596  cubic2  20690  quart1  20698  asinsinlem  20733  asinsin  20734  2efiatan  20760  pclogsum  21001  lgsneg  21105  vc0  22050  vcm  22052  vcnegneg  22055  nvpi  22157  honegneg  23311  opsqrlem6  23650  sto1i  23741  mdexchi  23840  cnre2csqlem  24310  subfacp1lem1  24867  ghomfo  25104  rankaltopb  25826  bpoly3  26106  bpoly4  26107  heiborlem6  26527  frlmup3  27231  dvsinexp  27718  stirlinglem1  27801  trlcoat  31522  cdlemk54  31757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator