Theorem 3eqtr3a 2478

Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.)

Hypotheses

Ref	Expression
3eqtr3a.1
3eqtr3a.2
3eqtr3a.3

Assertion

Ref	Expression
3eqtr3a

Proof of Theorem 3eqtr3a

Step	Hyp	Ref	Expression
1		3eqtr3a.2	. 2
2		3eqtr3a.1	. . 3
3		3eqtr3a.3	. . 3
4	2, 3	syl5eq 2466	. 2
5	1, 4	eqtr3d 2456	1

Syntax hints:  ->wi 4  =wceq 1687

This theorem is referenced by:  uneqin  3578  coi2  5326  foima  5595  f1imacnv  5627  fvsnun2  5883  fnsnsplit  5884  phplem4  7452  php3  7456  rankopb  8006  fin4en1  8425  fpwwe2  8756  winacard  8805  mul02lem1  9491  cnegex2  9497  crreczi  11930  hashinf  12049  hashcard  12066  cshw0  12372  cshwn  12375  sqrneglem  12697  rlimresb  12984  sinhval  13378  coshval  13379  absefib  13422  efieq1re  13423  sadcaddlem  13593  sadaddlem  13602  odngen  16013  frlmup3  17928  mat0op  18018  restopnb  18483  cnmpt2t  18950  volsup2  20785  plypf1  21421  pige3  21720  sineq0  21724  eflog  21769  logef  21771  cxpsqr  21889  cubic2  21984  quart1  21992  asinsinlem  22027  asinsin  22028  2efiatan  22054  pclogsum  22295  lgsneg  22399  vc0  23626  vcm  23628  vcnegneg  23631  nvpi  23733  honegneg  24889  opsqrlem6  25228  sto1i  25319  mdexchi  25418  cnre2csqlem  26049  subfacp1lem1  26770  ghomfo  27012  rankaltopb  27712  bpoly3  27903  bpoly4  27904  dvtan  28113  dvcncxp1  28148  dvasin  28151  heiborlem6  28386  iocunico  29259  dvsinexp  29461  stirlinglem1  29543  numclwlk1lem2fo  30362  trlcoat  33804  cdlemk54  34039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-12 1785  ax-ext 2403

This theorem depends on definitions:  df-bi 179  df-ex 1582  df-cleq 2415