Theorem 3eqtr3a 2485

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

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-cleq 2412

This theorem is referenced by:  uneqin  3721  coi2  5363  foima  5806  f1imacnv  5838  fvsnun2  6106  fnsnsplit  6107  phplem4  7751  php3  7755  rankopb  8313  fin4en1  8728  fpwwe2  9057  winacard  9106  mul02lem1  9798  cnegex2  9804  crreczi  12383  hashinf  12506  hashcard  12523  cshw0  12870  cshwn  12873  sqrtneglem  13298  rlimresb  13596  bpoly3  14078  bpoly4  14079  sinhval  14175  coshval  14176  absefib  14219  efieq1re  14220  sadcaddlem  14394  sadaddlem  14403  psgnsn  17113  odngen  17167  frlmup3  19295  mat0op  19381  restopnb  20128  cnmpt2t  20625  volsup2  22470  plypf1  23073  pige3  23376  sineq0  23380  eflog  23430  logef  23435  cxpsqrt  23552  dvcncxp1  23587  cubic2  23678  quart1  23686  asinsinlem  23721  asinsin  23722  2efiatan  23748  pclogsum  24045  lgsneg  24149  numclwlk1lem2fo  25709  vc0  26074  vcm  26076  vcnegneg  26079  nvpi  26181  honegneg  27335  opsqrlem6  27674  sto1i  27765  mdexchi  27864  cnre2csqlem  28596  subfacp1lem1  29731  ghomfo  30138  rankaltopb  30572  poimirlem23  31711  dvtan  31740  dvasin  31776  heiborlem6  31896  trlcoat  34043  cdlemk54  34278  iocunico  35842  snunioo1  37246  dvsinexp  37400  itgsubsticclem  37469  stirlinglem1  37553  fourierdlem80  37666  fourierdlem111  37697  sqwvfoura  37708  sqwvfourb  37709  fouriersw  37711  aacllem  39358