Theorem 3eqtr3a 2803

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	eqtrid 2790	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2780	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  uneqin  4209  coi2  6156  foima  6677  f1imacnv  6716  fvsnun1  7036  fnsnsplit  7038  phplem4  8895  php3  8899  rankopb  9541  fin4en1  9996  fpwwe2  10330  winacard  10379  mul02lem1  11081  cnegex2  11087  crreczi  13871  hashinf  13977  hashcard  13998  cshw0  14435  cshwn  14438  sqrtneglem  14906  rlimresb  15202  bpoly3  15696  bpoly4  15697  sinhval  15791  coshval  15792  absefib  15835  efieq1re  15836  sadcaddlem  16092  sadaddlem  16101  psgnsn  19043  odngen  19097  frlmup3  20917  mat0op  21476  restopnb  22234  cnmpt2t  22732  clmnegneg  24173  ncvspi  24225  volsup2  24674  plypf1  25278  pige3ALT  25581  sineq0  25585  eflog  25637  logef  25642  cxpsqrt  25763  dvcncxp1  25801  cubic2  25903  quart1  25911  asinsinlem  25946  asinsin  25947  2efiatan  25973  pclogsum  26268  lgsneg  26374  vc0  28837  vcm  28839  nvpi  28930  honegneg  30069  opsqrlem6  30408  sto1i  30499  mdexchi  30598  preiman0  30944  elrspunidl  31508  cnre2csqlem  31762  itgexpif  32486  subfacp1lem1  33041  rankaltopb  34208  poimirlem23  35727  dvtan  35754  dvasin  35788  heiborlem6  35901  trlcoat  38664  cdlemk54  38899  resubid  40312  sn-mul02  40343  iocunico  40958  relintab  41080  rfovcnvf1od  41501  ntrneifv3  41581  ntrneifv4  41584  clsneifv3  41609  clsneifv4  41610  neicvgfv  41620  snunioo1  42940  dvsinexp  43342  itgsubsticclem  43406  stirlinglem1  43505  fourierdlem80  43617  fourierdlem111  43648  sqwvfoura  43659  sqwvfourb  43660  fouriersw  43662  smfco  44223  aacllem  46391