Theorem 3eqtr2i 2774

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2i.1	⊢ 𝐴 = 𝐵
3eqtr2i.2	⊢ 𝐶 = 𝐵
3eqtr2i.3	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
3eqtr2i	⊢ 𝐴 = 𝐷

Proof of Theorem 3eqtr2i

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2771	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtri 2768	1 ⊢ 𝐴 = 𝐷

Syntax hints:   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  indif  4299  dfrab3  4338  iunidOLD  5084  cocnvcnv2  6289  fmptap  7204  cnvoprab  8101  fpar  8157  fodomr  9194  fodomfir  9396  jech9.3  9883  dju1dif  10242  alephadd  10646  distrnq  11030  ltanq  11040  ltrnq  11048  1p2e3  12436  halfpm6th  12514  numma  12802  numaddc  12806  6p5lem  12828  8p2e10  12838  binom2i  14261  faclbnd4lem1  14342  cats2cat  14911  0.999...  15929  flodddiv4  16461  6gcd4e2  16585  dfphi2  16821  mod2xnegi  17118  karatsuba  17131  1259lem1  17178  setc2obas  18161  oppgtopn  19396  symgplusg  19424  cmnbascntr  19847  mgptopn  20173  ply1plusg  22246  ply1vsca  22247  ply1mulr  22248  restcld  23201  cmpsublem  23428  kgentopon  23567  dfii5  24930  itg1climres  25769  pigt3  26578  ang180lem1  26870  1cubrlem  26902  quart1lem  26916  efiatan  26973  log2cnv  27005  log2ublem3  27009  1sgm2ppw  27262  ppiub  27266  bposlem8  27353  bposlem9  27354  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  bday1s  27894  addsasslem2  28055  seqsval  28312  pw2bday  28436  ax5seglem7  28968  wlknwwlksnbij  29921  2pthd  29973  3pthd  30206  ipidsq  30742  ipdirilem  30861  norm3difi  31179  polid2i  31189  pjclem3  32229  cvmdi  32356  indifundif  32554  dpmul  32877  tocyccntz  33137  ccfldextdgrr  33682  eulerpartlemt  34336  eulerpart  34347  ballotlem1  34451  ballotlemfval0  34460  ballotth  34502  hgt750lem  34628  hgt750lem2  34629  subfaclim  35156  kur14lem6  35179  quad3  35638  iexpire  35697  volsupnfl  37625  dfxrn2  38332  xrninxp  38348  ipiiie0  42413  sn-0tie0  42415  areaquad  43177  wallispilem4  45989  dirkertrigeqlem3  46021  dirkercncflem1  46024  fourierswlem  46151  fouriersw  46152  smflimsuplem8  46748  3exp4mod41  47490  41prothprm  47493  tgoldbachlt  47690  zlmodzxz0  48081  linevalexample  48124  mndtcco  48758