Theorem 3eqtr3a 2801

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  uneqin  4289  coi2  6283  foima  6825  f1imacnv  6864  fvsnun1  7202  fnsnsplit  7204  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  rankopb  9892  fin4en1  10349  fpwwe2  10683  winacard  10732  mul02lem1  11437  cnegex2  11443  crreczi  14267  hashinf  14374  hashcard  14394  cshw0  14832  cshwn  14835  sqrtneglem  15305  rlimresb  15601  bpoly3  16094  bpoly4  16095  sinhval  16190  coshval  16191  absefib  16234  efieq1re  16235  sadcaddlem  16494  sadaddlem  16503  qus0subgbas  19216  psgnsn  19538  odngen  19595  frlmup3  21820  mat0op  22425  restopnb  23183  cnmpt2t  23681  clmnegneg  25137  ncvspi  25190  volsup2  25640  plypf1  26251  pige3ALT  26562  sineq0  26566  eflog  26618  logef  26623  cxpsqrt  26745  dvcncxp1  26785  cubic2  26891  quart1  26899  asinsinlem  26934  asinsin  26935  2efiatan  26961  pclogsum  27259  lgsneg  27365  vc0  30593  vcm  30595  nvpi  30686  honegneg  31825  opsqrlem6  32164  sto1i  32255  mdexchi  32354  fmptunsnop  32709  preiman0  32719  elrspunidl  33456  cnre2csqlem  33909  itgexpif  34621  subfacp1lem1  35184  rankaltopb  35980  poimirlem23  37650  dvtan  37677  dvasin  37711  heiborlem6  37823  trlcoat  40725  cdlemk54  40960  readvcot  42394  resubid  42438  sn-mul02  42470  iocunico  43223  relintab  43596  rfovcnvf1od  44017  ntrneifv3  44095  ntrneifv4  44098  clsneifv3  44123  clsneifv4  44124  neicvgfv  44134  snunioo1  45525  dvsinexp  45926  dvnprodlem1  45961  itgsubsticclem  45990  stirlinglem1  46089  fourierdlem80  46201  fourierdlem111  46232  sqwvfoura  46243  sqwvfourb  46244  fouriersw  46246  saliinclf  46341  smfco  46817  aacllem  49320