Theorem 3eqtr3a 2532

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

Syntax hints:   -> wi 4   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459

This theorem is referenced by:  uneqin  3749  coi2  5524  foima  5800  f1imacnv  5832  fvsnun2  6098  fnsnsplit  6099  phplem4  7700  php3  7704  rankopb  8271  fin4en1  8690  fpwwe2  9022  winacard  9071  mul02lem1  9756  cnegex2  9762  crreczi  12260  hashinf  12379  hashcard  12396  cshw0  12731  cshwn  12734  sqrtneglem  13066  rlimresb  13354  sinhval  13753  coshval  13754  absefib  13797  efieq1re  13798  sadcaddlem  13969  sadaddlem  13978  psgnsn  16360  odngen  16412  frlmup3  18641  mat0op  18728  restopnb  19482  cnmpt2t  20001  volsup2  21841  plypf1  22436  pige3  22735  sineq0  22739  eflog  22789  logef  22791  cxpsqrt  22909  cubic2  23004  quart1  23012  asinsinlem  23047  asinsin  23048  2efiatan  23074  pclogsum  23315  lgsneg  23419  numclwlk1lem2fo  24869  vc0  25235  vcm  25237  vcnegneg  25240  nvpi  25342  honegneg  26498  opsqrlem6  26837  sto1i  26928  mdexchi  27027  cnre2csqlem  27643  subfacp1lem1  28374  ghomfo  28782  rankaltopb  29482  bpoly3  29673  bpoly4  29674  dvtan  29918  dvcncxp1  29953  dvasin  29956  heiborlem6  30142  iocunico  31010  dvsinexp  31465  itgsubsticclem  31520  stirlinglem1  31601  trlcoat  35736  cdlemk54  35971