Theorem 3eqtr3a 2802

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730

This theorem is referenced by:  uneqin  4212  coi2  6167  foima  6693  f1imacnv  6732  fvsnun1  7054  fnsnsplit  7056  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  rankopb  9610  fin4en1  10065  fpwwe2  10399  winacard  10448  mul02lem1  11151  cnegex2  11157  crreczi  13943  hashinf  14049  hashcard  14070  cshw0  14507  cshwn  14510  sqrtneglem  14978  rlimresb  15274  bpoly3  15768  bpoly4  15769  sinhval  15863  coshval  15864  absefib  15907  efieq1re  15908  sadcaddlem  16164  sadaddlem  16173  psgnsn  19128  odngen  19182  frlmup3  21007  mat0op  21568  restopnb  22326  cnmpt2t  22824  clmnegneg  24267  ncvspi  24320  volsup2  24769  plypf1  25373  pige3ALT  25676  sineq0  25680  eflog  25732  logef  25737  cxpsqrt  25858  dvcncxp1  25896  cubic2  25998  quart1  26006  asinsinlem  26041  asinsin  26042  2efiatan  26068  pclogsum  26363  lgsneg  26469  vc0  28936  vcm  28938  nvpi  29029  honegneg  30168  opsqrlem6  30507  sto1i  30598  mdexchi  30697  preiman0  31042  elrspunidl  31606  cnre2csqlem  31860  itgexpif  32586  subfacp1lem1  33141  rankaltopb  34281  poimirlem23  35800  dvtan  35827  dvasin  35861  heiborlem6  35974  trlcoat  38737  cdlemk54  38972  resubid  40391  sn-mul02  40422  iocunico  41042  relintab  41191  rfovcnvf1od  41612  ntrneifv3  41692  ntrneifv4  41695  clsneifv3  41720  clsneifv4  41721  neicvgfv  41731  snunioo1  43050  dvsinexp  43452  itgsubsticclem  43516  stirlinglem1  43615  fourierdlem80  43727  fourierdlem111  43758  sqwvfoura  43769  sqwvfourb  43770  fouriersw  43772  smfco  44336  aacllem  46505