Theorem 3eqtr3a 2789

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 2777	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2767	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  uneqin  4255  coi2  6239  foima  6780  f1imacnv  6819  fvsnun1  7159  fnsnsplit  7161  phplem2  9175  php3  9179  rankopb  9812  fin4en1  10269  fpwwe2  10603  winacard  10652  mul02lem1  11357  cnegex2  11363  crreczi  14200  hashinf  14307  hashcard  14327  cshw0  14766  cshwn  14769  sqrtneglem  15239  rlimresb  15538  bpoly3  16031  bpoly4  16032  sinhval  16129  coshval  16130  absefib  16173  efieq1re  16174  sadcaddlem  16434  sadaddlem  16443  qus0subgbas  19137  psgnsn  19457  odngen  19514  frlmup3  21716  mat0op  22313  restopnb  23069  cnmpt2t  23567  clmnegneg  25011  ncvspi  25063  volsup2  25513  plypf1  26124  pige3ALT  26436  sineq0  26440  eflog  26492  logef  26497  cxpsqrt  26619  dvcncxp1  26659  cubic2  26765  quart1  26773  asinsinlem  26808  asinsin  26809  2efiatan  26835  pclogsum  27133  lgsneg  27239  vc0  30510  vcm  30512  nvpi  30603  honegneg  31742  opsqrlem6  32081  sto1i  32172  mdexchi  32271  fmptunsnop  32630  preiman0  32640  elrspunidl  33406  cnre2csqlem  33907  itgexpif  34604  subfacp1lem1  35173  rankaltopb  35974  poimirlem23  37644  dvtan  37671  dvasin  37705  heiborlem6  37817  trlcoat  40724  cdlemk54  40959  readvcot  42359  resubid  42404  sn-mul02  42447  iocunico  43207  relintab  43579  rfovcnvf1od  44000  ntrneifv3  44078  ntrneifv4  44081  clsneifv3  44106  clsneifv4  44107  neicvgfv  44117  snunioo1  45517  dvsinexp  45916  dvnprodlem1  45951  itgsubsticclem  45980  stirlinglem1  46079  fourierdlem80  46191  fourierdlem111  46222  sqwvfoura  46233  sqwvfourb  46234  fouriersw  46236  saliinclf  46331  smfco  46807  2oppf  49125  aacllem  49794