Theorem 3eqtr3a 2796

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 2784	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2774	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 2709

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

This theorem is referenced by:  uneqin  4243  coi2  6230  foima  6759  f1imacnv  6798  fvsnun1  7138  fnsnsplit  7140  phplem2  9141  php3  9145  rankopb  9776  fin4en1  10231  fpwwe2  10566  winacard  10615  mul02lem1  11321  cnegex2  11327  crreczi  14163  hashinf  14270  hashcard  14290  cshw0  14729  cshwn  14732  sqrtneglem  15201  rlimresb  15500  bpoly3  15993  bpoly4  15994  sinhval  16091  coshval  16092  absefib  16135  efieq1re  16136  sadcaddlem  16396  sadaddlem  16405  qus0subgbas  19139  psgnsn  19461  odngen  19518  frlmup3  21767  mat0op  22375  restopnb  23131  cnmpt2t  23629  clmnegneg  25072  ncvspi  25124  volsup2  25574  plypf1  26185  pige3ALT  26497  sineq0  26501  eflog  26553  logef  26558  cxpsqrt  26680  dvcncxp1  26720  cubic2  26826  quart1  26834  asinsinlem  26869  asinsin  26870  2efiatan  26896  pclogsum  27194  lgsneg  27300  bdayfinbndlem1  28475  vc0  30662  vcm  30664  nvpi  30755  honegneg  31894  opsqrlem6  32233  sto1i  32324  mdexchi  32423  fmptunsnop  32790  preiman0  32800  elrspunidl  33521  cnre2csqlem  34088  itgexpif  34784  subfacp1lem1  35395  rankaltopb  36195  poimirlem23  37894  dvtan  37921  dvasin  37955  heiborlem6  38067  trlcoat  41099  cdlemk54  41334  readvcot  42734  resubid  42779  sn-mul02  42822  iocunico  43568  relintab  43939  rfovcnvf1od  44360  ntrneifv3  44438  ntrneifv4  44441  clsneifv3  44466  clsneifv4  44467  neicvgfv  44477  snunioo1  45872  dvsinexp  46269  dvnprodlem1  46304  itgsubsticclem  46333  stirlinglem1  46432  fourierdlem80  46544  fourierdlem111  46575  sqwvfoura  46586  sqwvfourb  46587  fouriersw  46589  saliinclf  46684  smfco  47160  2oppf  49491  aacllem  50160