Theorem 3eqtr3a 2799

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  uneqin  4295  coi2  6285  foima  6826  f1imacnv  6865  fvsnun1  7202  fnsnsplit  7204  phplem2  9243  php3  9247  phplem4OLD  9255  php3OLD  9259  rankopb  9890  fin4en1  10347  fpwwe2  10681  winacard  10730  mul02lem1  11435  cnegex2  11441  crreczi  14264  hashinf  14371  hashcard  14391  cshw0  14829  cshwn  14832  sqrtneglem  15302  rlimresb  15598  bpoly3  16091  bpoly4  16092  sinhval  16187  coshval  16188  absefib  16231  efieq1re  16232  sadcaddlem  16491  sadaddlem  16500  qus0subgbas  19229  psgnsn  19553  odngen  19610  frlmup3  21838  mat0op  22441  restopnb  23199  cnmpt2t  23697  clmnegneg  25151  ncvspi  25204  volsup2  25654  plypf1  26266  pige3ALT  26577  sineq0  26581  eflog  26633  logef  26638  cxpsqrt  26760  dvcncxp1  26800  cubic2  26906  quart1  26914  asinsinlem  26949  asinsin  26950  2efiatan  26976  pclogsum  27274  lgsneg  27380  vc0  30603  vcm  30605  nvpi  30696  honegneg  31835  opsqrlem6  32174  sto1i  32265  mdexchi  32364  fmptunsnop  32715  preiman0  32725  elrspunidl  33436  cnre2csqlem  33871  itgexpif  34600  subfacp1lem1  35164  rankaltopb  35961  poimirlem23  37630  dvtan  37657  dvasin  37691  heiborlem6  37803  trlcoat  40706  cdlemk54  40941  resubid  42415  sn-mul02  42447  iocunico  43200  relintab  43573  rfovcnvf1od  43994  ntrneifv3  44072  ntrneifv4  44075  clsneifv3  44100  clsneifv4  44101  neicvgfv  44111  snunioo1  45465  dvsinexp  45867  dvnprodlem1  45902  itgsubsticclem  45931  stirlinglem1  46030  fourierdlem80  46142  fourierdlem111  46173  sqwvfoura  46184  sqwvfourb  46185  fouriersw  46187  saliinclf  46282  smfco  46758  aacllem  49032