Theorem 3eqtr3a 2822

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  uneqin  4237  coi2  6286  foima  6831  f1imacnv  6871  fvsnun1  7218  fnsnsplit  7220  phplem2  9258  php3  9262  rankopb  9903  fin4en1  10426  fpwwe2  10767  winacard  10816  mul02lem1  11525  cnegex2  11531  crreczi  14413  hashinf  14520  hashcard  14540  cshw0  14987  cshwn  14990  sqrtneglem  15476  rlimresb  15776  bpoly3  16268  bpoly4  16269  sinhval  16366  coshval  16367  absefib  16410  efieq1re  16411  sadcaddlem  16671  sadaddlem  16680  qus0subgbas  19463  psgnsn  19785  odngen  19842  frlmup3  22161  mat0op  22789  restopnb  23548  cnmpt2t  24047  clmnegneg  25480  ncvspi  25532  volsup2  25981  plypf1  26586  pige3ALT  26905  sineq0  26909  eflog  26961  logef  26966  cxpsqrt  27088  dvcncxp1  27128  cubic2  27233  quart1  27241  asinsinlem  27276  asinsin  27277  2efiatan  27303  pclogsum  27599  lgsneg  27705  bdayfinbndlem1  28910  vc0  31233  vcm  31235  nvpi  31326  honegneg  32465  opsqrlem6  32804  sto1i  32895  mdexchi  32994  fmptunsnop  33390  preiman0  33400  elrspunidl  34082  cnre2csqlem  34653  itgexpif  35346  subfacp1lem1  36152  rankaltopb  36959  poimirlem23  38829  dvtan  38856  dvasin  38890  heiborlem6  39016  trlcoat  42046  cdlemk54  42281  readvcot  43681  resubid  43726  sn-mul02  43782  iocunico  44474  relintab  44845  rfovcnvf1od  45265  ntrneifv3  45343  ntrneifv4  45346  clsneifv3  45371  clsneifv4  45372  neicvgfv  45382  snunioo1  46797  dvsinexp  47194  dvnprodlem1  47229  itgsubsticclem  47258  stirlinglem1  47357  fourierdlem80  47469  fourierdlem111  47500  sqwvfoura  47511  sqwvfourb  47512  fouriersw  47514  saliinclf  47609  smfco  48085  2oppf  50579  aacllem  51367