Theorem 3eqtr3a 2497

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

Syntax hints:   -> wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434

This theorem is referenced by:  uneqin  3598  coi2  5351  foima  5622  f1imacnv  5654  fvsnun2  5911  fnsnsplit  5912  phplem4  7489  php3  7493  rankopb  8055  fin4en1  8474  fpwwe2  8806  winacard  8855  mul02lem1  9541  cnegex2  9547  crreczi  11985  hashinf  12104  hashcard  12121  cshw0  12427  cshwn  12430  sqrneglem  12752  rlimresb  13039  sinhval  13434  coshval  13435  absefib  13478  efieq1re  13479  sadcaddlem  13649  sadaddlem  13658  odngen  16069  frlmup3  18187  mat0op  18279  restopnb  18738  cnmpt2t  19205  volsup2  21044  plypf1  21639  pige3  21938  sineq0  21942  eflog  21987  logef  21989  cxpsqr  22107  cubic2  22202  quart1  22210  asinsinlem  22245  asinsin  22246  2efiatan  22272  pclogsum  22513  lgsneg  22617  vc0  23882  vcm  23884  vcnegneg  23887  nvpi  23989  honegneg  25145  opsqrlem6  25484  sto1i  25575  mdexchi  25674  cnre2csqlem  26276  subfacp1lem1  26997  ghomfo  27239  rankaltopb  27939  bpoly3  28130  bpoly4  28131  dvtan  28367  dvcncxp1  28402  dvasin  28405  heiborlem6  28640  iocunico  29511  dvsinexp  29712  stirlinglem1  29794  numclwlk1lem2fo  30613  psgnsn  30688  trlcoat  34089  cdlemk54  34324