Theorem 3eqtr3a 2820

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

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  uneqin  4239  coi2  6246  foima  6778  f1imacnv  6818  fvsnun1  7161  fnsnsplit  7163  phplem2  9167  php3  9171  rankopb  9804  fin4en1  10260  fpwwe2  10595  winacard  10644  mul02lem1  11353  cnegex2  11359  crreczi  14235  hashinf  14342  hashcard  14362  cshw0  14801  cshwn  14804  sqrtneglem  15284  rlimresb  15583  bpoly3  16079  bpoly4  16080  sinhval  16177  coshval  16178  absefib  16221  efieq1re  16222  sadcaddlem  16482  sadaddlem  16491  qus0subgbas  19230  psgnsn  19551  odngen  19608  frlmup3  21840  mat0op  22467  restopnb  23223  cnmpt2t  23721  clmnegneg  25154  ncvspi  25206  volsup2  25655  plypf1  26260  pige3ALT  26573  sineq0  26577  eflog  26629  logef  26634  cxpsqrt  26756  dvcncxp1  26796  cubic2  26901  quart1  26909  asinsinlem  26944  asinsin  26945  2efiatan  26971  pclogsum  27267  lgsneg  27373  bdayfinbndlem1  28548  vc0  30734  vcm  30736  nvpi  30827  honegneg  31966  opsqrlem6  32305  sto1i  32396  mdexchi  32495  fmptunsnop  32863  preiman0  32873  elrspunidl  33575  cnre2csqlem  34168  itgexpif  34861  subfacp1lem1  35490  rankaltopb  36290  poimirlem23  38103  dvtan  38130  dvasin  38164  heiborlem6  38276  trlcoat  41308  cdlemk54  41543  readvcot  42934  resubid  42979  sn-mul02  43035  iocunico  43749  relintab  44120  rfovcnvf1od  44541  ntrneifv3  44619  ntrneifv4  44622  clsneifv3  44647  clsneifv4  44648  neicvgfv  44658  snunioo1  46049  dvsinexp  46446  dvnprodlem1  46481  itgsubsticclem  46510  stirlinglem1  46609  fourierdlem80  46721  fourierdlem111  46752  sqwvfoura  46763  sqwvfourb  46764  fouriersw  46766  saliinclf  46861  smfco  47337  2oppf  49714  aacllem  50383