Theorem 3eqtr3a 2680

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

Syntax hints:   → wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  uneqin  3878  coi2  5652  foima  6120  f1imacnv  6153  fvsnun2  6449  fnsnsplit  6450  phplem4  8142  php3  8146  rankopb  8715  fin4en1  9131  fpwwe2  9465  winacard  9514  mul02lem1  10212  cnegex2  10218  crreczi  12989  hashinf  13122  hashcard  13146  cshw0  13540  cshwn  13543  sqrtneglem  14007  rlimresb  14296  bpoly3  14789  bpoly4  14790  sinhval  14884  coshval  14885  absefib  14928  efieq1re  14929  sadcaddlem  15179  sadaddlem  15188  psgnsn  17940  odngen  17992  frlmup3  20139  mat0op  20225  restopnb  20979  cnmpt2t  21476  clmnegneg  22904  ncvspi  22956  volsup2  23373  plypf1  23968  pige3  24269  sineq0  24273  eflog  24323  logef  24328  cxpsqrt  24449  dvcncxp1  24484  cubic2  24575  quart1  24583  asinsinlem  24618  asinsin  24619  2efiatan  24645  pclogsum  24940  lgsneg  25046  numclwlk1lem2fo  27228  vc0  27429  vcm  27431  nvpi  27522  honegneg  28665  opsqrlem6  29004  sto1i  29095  mdexchi  29194  cnre2csqlem  29956  itgexpif  30684  subfacp1lem1  31161  rankaltopb  32086  poimirlem23  33432  dvtan  33460  dvasin  33496  heiborlem6  33615  trlcoat  36011  cdlemk54  36246  iocunico  37796  relintab  37889  rfovcnvf1od  38298  ntrneifv3  38380  ntrneifv4  38383  clsneifv3  38408  clsneifv4  38409  neicvgfv  38419  snunioo1  39738  dvsinexp  40125  itgsubsticclem  40191  stirlinglem1  40291  fourierdlem80  40403  fourierdlem111  40434  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  aacllem  42547