Theorem 3eqtr3a 2520

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 2508	. 2 |- ( ph -> A = D )
5	1, 4	eqtr3d 2498	1 |- ( ph -> C = D )

Syntax hints:   -> wi 4   = wceq 1455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-cleq 2455

This theorem is referenced by:  uneqin  3706  coi2  5375  foima  5825  f1imacnv  5857  fvsnun2  6129  fnsnsplit  6130  phplem4  7785  php3  7789  rankopb  8354  fin4en1  8770  fpwwe2  9099  winacard  9148  mul02lem1  9840  cnegex2  9846  crreczi  12435  hashinf  12558  hashcard  12575  cshw0  12939  cshwn  12942  sqrtneglem  13385  rlimresb  13684  bpoly3  14166  bpoly4  14167  sinhval  14263  coshval  14264  absefib  14307  efieq1re  14308  sadcaddlem  14486  sadaddlem  14495  psgnsn  17216  odngen  17281  frlmup3  19413  mat0op  19499  restopnb  20246  cnmpt2t  20743  volsup2  22619  plypf1  23222  pige3  23528  sineq0  23532  eflog  23582  logef  23587  cxpsqrt  23704  dvcncxp1  23739  cubic2  23830  quart1  23838  asinsinlem  23873  asinsin  23874  2efiatan  23900  pclogsum  24199  lgsneg  24303  numclwlk1lem2fo  25879  vc0  26244  vcm  26246  vcnegneg  26249  nvpi  26351  honegneg  27515  opsqrlem6  27854  sto1i  27945  mdexchi  28044  cnre2csqlem  28767  subfacp1lem1  29952  ghomfo  30359  rankaltopb  30796  poimirlem23  32009  dvtan  32038  dvasin  32074  heiborlem6  32194  trlcoat  34336  cdlemk54  34571  iocunico  36141  relintab  36235  snunioo1  37698  dvsinexp  37866  itgsubsticclem  37938  stirlinglem1  38037  fourierdlem80  38151  fourierdlem111  38182  sqwvfoura  38193  sqwvfourb  38194  fouriersw  38196  aacllem  40909