Theorem 3eqtr3a 2795

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  uneqin  4241  coi2  6222  foima  6751  f1imacnv  6790  fvsnun1  7128  fnsnsplit  7130  phplem2  9129  php3  9133  rankopb  9764  fin4en1  10219  fpwwe2  10554  winacard  10603  mul02lem1  11309  cnegex2  11315  crreczi  14151  hashinf  14258  hashcard  14278  cshw0  14717  cshwn  14720  sqrtneglem  15189  rlimresb  15488  bpoly3  15981  bpoly4  15982  sinhval  16079  coshval  16080  absefib  16123  efieq1re  16124  sadcaddlem  16384  sadaddlem  16393  qus0subgbas  19127  psgnsn  19449  odngen  19506  frlmup3  21755  mat0op  22363  restopnb  23119  cnmpt2t  23617  clmnegneg  25060  ncvspi  25112  volsup2  25562  plypf1  26173  pige3ALT  26485  sineq0  26489  eflog  26541  logef  26546  cxpsqrt  26668  dvcncxp1  26708  cubic2  26814  quart1  26822  asinsinlem  26857  asinsin  26858  2efiatan  26884  pclogsum  27182  lgsneg  27288  bdayfinbndlem1  28463  vc0  30649  vcm  30651  nvpi  30742  honegneg  31881  opsqrlem6  32220  sto1i  32311  mdexchi  32410  fmptunsnop  32779  preiman0  32789  elrspunidl  33509  cnre2csqlem  34067  itgexpif  34763  subfacp1lem1  35373  rankaltopb  36173  poimirlem23  37840  dvtan  37867  dvasin  37901  heiborlem6  38013  trlcoat  40979  cdlemk54  41214  readvcot  42615  resubid  42660  sn-mul02  42703  iocunico  43449  relintab  43820  rfovcnvf1od  44241  ntrneifv3  44319  ntrneifv4  44322  clsneifv3  44347  clsneifv4  44348  neicvgfv  44358  snunioo1  45754  dvsinexp  46151  dvnprodlem1  46186  itgsubsticclem  46215  stirlinglem1  46314  fourierdlem80  46426  fourierdlem111  46457  sqwvfoura  46468  sqwvfourb  46469  fouriersw  46471  saliinclf  46566  smfco  47042  2oppf  49373  aacllem  50042