Theorem 3eqtr3a 2819

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  uneqin  4233  coi2  6267  foima  6804  f1imacnv  6844  fvsnun1  7189  fnsnsplit  7191  phplem2  9225  php3  9229  rankopb  9871  fin4en1  10392  fpwwe2  10733  winacard  10782  mul02lem1  11491  cnegex2  11497  crreczi  14377  hashinf  14484  hashcard  14504  cshw0  14951  cshwn  14954  sqrtneglem  15440  rlimresb  15739  bpoly3  16231  bpoly4  16232  sinhval  16329  coshval  16330  absefib  16373  efieq1re  16374  sadcaddlem  16634  sadaddlem  16643  qus0subgbas  19420  psgnsn  19741  odngen  19798  frlmup3  22113  mat0op  22741  restopnb  23500  cnmpt2t  23999  clmnegneg  25432  ncvspi  25484  volsup2  25933  plypf1  26538  pige3ALT  26855  sineq0  26859  eflog  26911  logef  26916  cxpsqrt  27038  dvcncxp1  27078  cubic2  27183  quart1  27191  asinsinlem  27226  asinsin  27227  2efiatan  27253  pclogsum  27549  lgsneg  27655  bdayfinbndlem1  28860  vc0  31183  vcm  31185  nvpi  31276  honegneg  32415  opsqrlem6  32754  sto1i  32845  mdexchi  32944  fmptunsnop  33342  preiman0  33352  elrspunidl  34026  cnre2csqlem  34590  itgexpif  35283  subfacp1lem1  36032  rankaltopb  36838  poimirlem23  38668  dvtan  38695  dvasin  38729  heiborlem6  38857  trlcoat  41887  cdlemk54  42122  readvcot  43522  resubid  43567  sn-mul02  43623  iocunico  44320  relintab  44691  rfovcnvf1od  45111  ntrneifv3  45189  ntrneifv4  45192  clsneifv3  45217  clsneifv4  45218  neicvgfv  45228  snunioo1  46631  dvsinexp  47028  dvnprodlem1  47063  itgsubsticclem  47092  stirlinglem1  47191  fourierdlem80  47303  fourierdlem111  47334  sqwvfoura  47345  sqwvfourb  47346  fouriersw  47348  saliinclf  47443  smfco  47919  2oppf  50355  aacllem  51121