Theorem 3eqtr3a 2499

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

Step	Hyp	Ref	Expression
1		3eqtr3a.2	. 2 |- ( ph -> A = C )
2		3eqtr3a.1	. . 3 |- A = B
3		3eqtr3a.3	. . 3 |- ( ph -> B = D )
4	2, 3	syl5eq 2487	. 2 |- ( ph -> A = D )
5	1, 4	eqtr3d 2477	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436

This theorem is referenced by:  uneqin  3622  coi2  5375  foima  5646  f1imacnv  5678  fvsnun2  5935  fnsnsplit  5936  phplem4  7514  php3  7518  rankopb  8080  fin4en1  8499  fpwwe2  8831  winacard  8880  mul02lem1  9566  cnegex2  9572  crreczi  12010  hashinf  12129  hashcard  12146  cshw0  12452  cshwn  12455  sqrneglem  12777  rlimresb  13064  sinhval  13459  coshval  13460  absefib  13503  efieq1re  13504  sadcaddlem  13674  sadaddlem  13683  odngen  16097  frlmup3  18250  mat0op  18342  restopnb  18801  cnmpt2t  19268  volsup2  21107  plypf1  21702  pige3  22001  sineq0  22005  eflog  22050  logef  22052  cxpsqr  22170  cubic2  22265  quart1  22273  asinsinlem  22308  asinsin  22309  2efiatan  22335  pclogsum  22576  lgsneg  22680  vc0  23969  vcm  23971  vcnegneg  23974  nvpi  24076  honegneg  25232  opsqrlem6  25571  sto1i  25662  mdexchi  25761  cnre2csqlem  26362  subfacp1lem1  27089  ghomfo  27332  rankaltopb  28032  bpoly3  28223  bpoly4  28224  dvtan  28468  dvcncxp1  28503  dvasin  28506  heiborlem6  28741  iocunico  29612  dvsinexp  29813  stirlinglem1  29895  numclwlk1lem2fo  30714  psgnsn  30801  trlcoat  34463  cdlemk54  34698