Theorem 3eqtr3a 2790

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 2778	. 2 ⊢ (𝜑 → 𝐴 = 𝐷)
5	1, 4	eqtr3d 2768	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 2121  ax-ext 2703

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

This theorem is referenced by:  uneqin  4234  coi2  6206  foima  6735  f1imacnv  6774  fvsnun1  7111  fnsnsplit  7113  phplem2  9109  php3  9113  rankopb  9740  fin4en1  10195  fpwwe2  10529  winacard  10578  mul02lem1  11284  cnegex2  11290  crreczi  14130  hashinf  14237  hashcard  14257  cshw0  14696  cshwn  14699  sqrtneglem  15168  rlimresb  15467  bpoly3  15960  bpoly4  15961  sinhval  16058  coshval  16059  absefib  16102  efieq1re  16103  sadcaddlem  16363  sadaddlem  16372  qus0subgbas  19105  psgnsn  19427  odngen  19484  frlmup3  21732  mat0op  22329  restopnb  23085  cnmpt2t  23583  clmnegneg  25026  ncvspi  25078  volsup2  25528  plypf1  26139  pige3ALT  26451  sineq0  26455  eflog  26507  logef  26512  cxpsqrt  26634  dvcncxp1  26674  cubic2  26780  quart1  26788  asinsinlem  26823  asinsin  26824  2efiatan  26850  pclogsum  27148  lgsneg  27254  vc0  30546  vcm  30548  nvpi  30639  honegneg  31778  opsqrlem6  32117  sto1i  32208  mdexchi  32307  fmptunsnop  32673  preiman0  32683  elrspunidl  33385  cnre2csqlem  33915  itgexpif  34611  subfacp1lem1  35215  rankaltopb  36013  poimirlem23  37683  dvtan  37710  dvasin  37744  heiborlem6  37856  trlcoat  40762  cdlemk54  40997  readvcot  42397  resubid  42442  sn-mul02  42485  iocunico  43244  relintab  43616  rfovcnvf1od  44037  ntrneifv3  44115  ntrneifv4  44118  clsneifv3  44143  clsneifv4  44144  neicvgfv  44154  snunioo1  45552  dvsinexp  45949  dvnprodlem1  45984  itgsubsticclem  46013  stirlinglem1  46112  fourierdlem80  46224  fourierdlem111  46255  sqwvfoura  46266  sqwvfourb  46267  fouriersw  46269  saliinclf  46364  smfco  46840  2oppf  49164  aacllem  49833