Theorem 3eqtr3a 2508

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

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

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

This theorem is referenced by:  uneqin  3734  coi2  5514  foima  5790  f1imacnv  5822  fvsnun2  6092  fnsnsplit  6093  phplem4  7701  php3  7705  rankopb  8273  fin4en1  8692  fpwwe2  9024  winacard  9073  mul02lem1  9759  cnegex2  9765  crreczi  12270  hashinf  12389  hashcard  12406  cshw0  12744  cshwn  12747  sqrtneglem  13079  rlimresb  13367  sinhval  13766  coshval  13767  absefib  13810  efieq1re  13811  sadcaddlem  13984  sadaddlem  13993  psgnsn  16419  odngen  16471  frlmup3  18707  mat0op  18794  restopnb  19549  cnmpt2t  20047  volsup2  21887  plypf1  22482  pige3  22782  sineq0  22786  eflog  22836  logef  22838  cxpsqrt  22956  cubic2  23051  quart1  23059  asinsinlem  23094  asinsin  23095  2efiatan  23121  pclogsum  23362  lgsneg  23466  numclwlk1lem2fo  24967  vc0  25334  vcm  25336  vcnegneg  25339  nvpi  25441  honegneg  26597  opsqrlem6  26936  sto1i  27027  mdexchi  27126  cnre2csqlem  27765  subfacp1lem1  28496  ghomfo  28904  rankaltopb  29604  bpoly3  29795  bpoly4  29796  dvtan  30040  dvcncxp1  30075  dvasin  30078  heiborlem6  30287  iocunico  31154  snunioo1  31488  dvsinexp  31609  itgsubsticclem  31664  stirlinglem1  31745  fourierdlem80  31858  fourierdlem111  31889  sqwvfoura  31900  sqwvfourb  31901  fouriersw  31903  trlcoat  36189  cdlemk54  36424