Theorem 3eqtr3a 2857

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

Syntax hints:   → wi 4   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  uneqin  4205  coi2  6083  foima  6570  f1imacnv  6606  fvsnun1  6921  fnsnsplit  6923  phplem4  8683  php3  8687  rankopb  9265  fin4en1  9720  fpwwe2  10054  winacard  10103  mul02lem1  10805  cnegex2  10811  crreczi  13585  hashinf  13691  hashcard  13712  cshw0  14147  cshwn  14150  sqrtneglem  14618  rlimresb  14914  bpoly3  15404  bpoly4  15405  sinhval  15499  coshval  15500  absefib  15543  efieq1re  15544  sadcaddlem  15796  sadaddlem  15805  psgnsn  18640  odngen  18694  frlmup3  20489  mat0op  21024  restopnb  21780  cnmpt2t  22278  clmnegneg  23709  ncvspi  23761  volsup2  24209  plypf1  24809  pige3ALT  25112  sineq0  25116  eflog  25168  logef  25173  cxpsqrt  25294  dvcncxp1  25332  cubic2  25434  quart1  25442  asinsinlem  25477  asinsin  25478  2efiatan  25504  pclogsum  25799  lgsneg  25905  vc0  28357  vcm  28359  nvpi  28450  honegneg  29589  opsqrlem6  29928  sto1i  30019  mdexchi  30118  preiman0  30469  elrspunidl  31014  cnre2csqlem  31263  itgexpif  31987  subfacp1lem1  32539  rankaltopb  33553  poimirlem23  35080  dvtan  35107  dvasin  35141  heiborlem6  35254  trlcoat  38019  cdlemk54  38254  resubid  39546  sn-mul02  39577  iocunico  40161  relintab  40283  rfovcnvf1od  40705  ntrneifv3  40785  ntrneifv4  40788  clsneifv3  40813  clsneifv4  40814  neicvgfv  40824  snunioo1  42149  dvsinexp  42553  itgsubsticclem  42617  stirlinglem1  42716  fourierdlem80  42828  fourierdlem111  42859  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  aacllem  45329