Theorem 3eqtr3a 2522

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 2510	. 2
5	1, 4	eqtr3d 2500	1

Syntax hints:  ->wi 4  =wceq 1395

This theorem is referenced by:  uneqin  3748  coi2  5529  foima  5805  f1imacnv  5837  fvsnun2  6107  fnsnsplit  6108  phplem4  7719  php3  7723  rankopb  8291  fin4en1  8710  fpwwe2  9042  winacard  9091  mul02lem1  9777  cnegex2  9783  crreczi  12291  hashinf  12410  hashcard  12427  cshw0  12765  cshwn  12768  sqrtneglem  13100  rlimresb  13388  sinhval  13889  coshval  13890  absefib  13933  efieq1re  13934  sadcaddlem  14107  sadaddlem  14116  psgnsn  16545  odngen  16597  frlmup3  18834  mat0op  18921  restopnb  19676  cnmpt2t  20174  volsup2  22014  plypf1  22609  pige3  22910  sineq0  22914  eflog  22964  logef  22966  cxpsqrt  23084  cubic2  23179  quart1  23187  asinsinlem  23222  asinsin  23223  2efiatan  23249  pclogsum  23490  lgsneg  23594  numclwlk1lem2fo  25095  vc0  25462  vcm  25464  vcnegneg  25467  nvpi  25569  honegneg  26725  opsqrlem6  27064  sto1i  27155  mdexchi  27254  cnre2csqlem  27892  subfacp1lem1  28623  ghomfo  29031  rankaltopb  29629  bpoly3  29820  bpoly4  29821  dvtan  30065  dvcncxp1  30100  dvasin  30103  heiborlem6  30312  iocunico  31178  snunioo1  31552  dvsinexp  31705  itgsubsticclem  31774  stirlinglem1  31856  fourierdlem80  31969  fourierdlem111  32000  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  aacllem  33216  trlcoat  36449  cdlemk54  36684

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

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