Theorem 3eqtr3a 2795

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  uneqin  4229  coi2  6228  foima  6757  f1imacnv  6796  fvsnun1  7137  fnsnsplit  7139  phplem2  9139  php3  9143  rankopb  9776  fin4en1  10231  fpwwe2  10566  winacard  10615  mul02lem1  11322  cnegex2  11328  crreczi  14190  hashinf  14297  hashcard  14317  cshw0  14756  cshwn  14759  sqrtneglem  15228  rlimresb  15527  bpoly3  16023  bpoly4  16024  sinhval  16121  coshval  16122  absefib  16165  efieq1re  16166  sadcaddlem  16426  sadaddlem  16435  qus0subgbas  19173  psgnsn  19495  odngen  19552  frlmup3  21780  mat0op  22384  restopnb  23140  cnmpt2t  23638  clmnegneg  25071  ncvspi  25123  volsup2  25572  plypf1  26177  pige3ALT  26484  sineq0  26488  eflog  26540  logef  26545  cxpsqrt  26667  dvcncxp1  26707  cubic2  26812  quart1  26820  asinsinlem  26855  asinsin  26856  2efiatan  26882  pclogsum  27178  lgsneg  27284  bdayfinbndlem1  28459  vc0  30645  vcm  30647  nvpi  30738  honegneg  31877  opsqrlem6  32216  sto1i  32307  mdexchi  32406  fmptunsnop  32773  preiman0  32783  elrspunidl  33488  cnre2csqlem  34054  itgexpif  34750  subfacp1lem1  35361  rankaltopb  36161  poimirlem23  37964  dvtan  37991  dvasin  38025  heiborlem6  38137  trlcoat  41169  cdlemk54  41404  readvcot  42796  resubid  42841  sn-mul02  42897  iocunico  43639  relintab  44010  rfovcnvf1od  44431  ntrneifv3  44509  ntrneifv4  44512  clsneifv3  44537  clsneifv4  44538  neicvgfv  44548  snunioo1  45942  dvsinexp  46339  dvnprodlem1  46374  itgsubsticclem  46403  stirlinglem1  46502  fourierdlem80  46614  fourierdlem111  46645  sqwvfoura  46656  sqwvfourb  46657  fouriersw  46659  saliinclf  46754  smfco  47230  2oppf  49607  aacllem  50276