Theorem 3eqtr3a 2792

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

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

This theorem is referenced by:  uneqin  4238  coi2  6219  foima  6748  f1imacnv  6787  fvsnun1  7125  fnsnsplit  7127  phplem2  9125  php3  9129  rankopb  9756  fin4en1  10211  fpwwe2  10545  winacard  10594  mul02lem1  11300  cnegex2  11306  crreczi  14142  hashinf  14249  hashcard  14269  cshw0  14708  cshwn  14711  sqrtneglem  15180  rlimresb  15479  bpoly3  15972  bpoly4  15973  sinhval  16070  coshval  16071  absefib  16114  efieq1re  16115  sadcaddlem  16375  sadaddlem  16384  qus0subgbas  19118  psgnsn  19440  odngen  19497  frlmup3  21746  mat0op  22354  restopnb  23110  cnmpt2t  23608  clmnegneg  25051  ncvspi  25103  volsup2  25553  plypf1  26164  pige3ALT  26476  sineq0  26480  eflog  26532  logef  26537  cxpsqrt  26659  dvcncxp1  26699  cubic2  26805  quart1  26813  asinsinlem  26848  asinsin  26849  2efiatan  26875  pclogsum  27173  lgsneg  27279  vc0  30575  vcm  30577  nvpi  30668  honegneg  31807  opsqrlem6  32146  sto1i  32237  mdexchi  32336  fmptunsnop  32705  preiman0  32715  elrspunidl  33437  cnre2csqlem  33995  itgexpif  34691  subfacp1lem1  35295  rankaltopb  36095  poimirlem23  37756  dvtan  37783  dvasin  37817  heiborlem6  37929  trlcoat  40895  cdlemk54  41130  readvcot  42534  resubid  42579  sn-mul02  42622  iocunico  43368  relintab  43740  rfovcnvf1od  44161  ntrneifv3  44239  ntrneifv4  44242  clsneifv3  44267  clsneifv4  44268  neicvgfv  44278  snunioo1  45674  dvsinexp  46071  dvnprodlem1  46106  itgsubsticclem  46135  stirlinglem1  46234  fourierdlem80  46346  fourierdlem111  46377  sqwvfoura  46388  sqwvfourb  46389  fouriersw  46391  saliinclf  46486  smfco  46962  2oppf  49293  aacllem  49962