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

Theorem 3eqtr3a 2491
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 2479 . 2  |-  ( ph  ->  A  =  D )
51, 4eqtr3d 2469 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  uneqin  3584  coi2  5377  foima  5649  f1imacnv  5682  fvsnun2  5920  fnsnsplit  5921  phplem4  7280  php3  7284  rankopb  7767  fin4en1  8178  fpwwe2  8507  winacard  8556  mul02lem1  9231  cnegex2  9237  crreczi  11492  hashinf  11611  hashcard  11626  sqrneglem  12060  rlimresb  12347  sinhval  12743  coshval  12744  absefib  12787  efieq1re  12788  sadcaddlem  12957  sadaddlem  12966  odngen  15199  restopnb  17227  cnmpt2t  17693  volsup2  19485  plypf1  20119  pige3  20413  sineq0  20417  eflog  20462  logef  20464  cxpsqr  20582  cubic2  20676  quart1  20684  asinsinlem  20719  asinsin  20720  2efiatan  20746  pclogsum  20987  lgsneg  21091  vc0  22036  vcm  22038  vcnegneg  22041  nvpi  22143  honegneg  23297  opsqrlem6  23636  sto1i  23727  mdexchi  23826  cnre2csqlem  24296  subfacp1lem1  24853  ghomfo  25090  rankaltopb  25772  bpoly3  26052  bpoly4  26053  heiborlem6  26462  frlmup3  27167  dvsinexp  27654  stirlinglem1  27737  trlcoat  31359  cdlemk54  31594
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator