Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr2i Structured version   Visualization version   GIF version

Theorem 3eqtr2i 2827
 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
StepHypRef Expression
1 3eqtr2i.1 . . 3 𝐴 = 𝐵
2 3eqtr2i.2 . . 3 𝐶 = 𝐵
31, 2eqtr4i 2824 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtri 2821 1 𝐴 = 𝐷
 Colors of variables: wff setvar class Syntax hints:   = 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:  indif  4196  dfrab3  4230  iunid  4947  cocnvcnv2  6078  fmptap  6909  cnvoprab  7742  fpar  7796  fodomr  8654  jech9.3  9229  dju1dif  9585  alephadd  9990  distrnq  10374  ltanq  10384  ltrnq  10392  1p2e3  11770  halfpm6th  11848  numma  12132  numaddc  12136  6p5lem  12158  8p2e10  12168  binom2i  13572  faclbnd4lem1  13651  cats2cat  14217  0.999...  15231  flodddiv4  15756  6gcd4e2  15878  dfphi2  16103  mod2xnegi  16399  karatsuba  16412  1259lem1  16458  oppgtopn  18476  symgplusg  18506  mgptopn  19244  ply1plusg  20861  ply1vsca  20862  ply1mulr  20863  restcld  21784  cmpsublem  22011  kgentopon  22150  dfii5  23497  itg1climres  24325  pigt3  25117  ang180lem1  25402  1cubrlem  25434  quart1lem  25448  efiatan  25505  log2cnv  25537  log2ublem3  25541  1sgm2ppw  25791  ppiub  25795  bposlem8  25882  bposlem9  25883  2lgsoddprmlem3c  26003  2lgsoddprmlem3d  26004  ax5seglem7  26736  wlknwwlksnbij  27681  2pthd  27733  3pthd  27966  ipidsq  28500  ipdirilem  28619  norm3difi  28937  polid2i  28947  pjclem3  29987  cvmdi  30114  indifundif  30304  dpmul  30622  tocyccntz  30843  ccfldextdgrr  31157  eulerpartlemt  31751  eulerpart  31762  ballotlem1  31866  ballotlemfval0  31875  ballotth  31917  hgt750lem  32044  hgt750lem2  32045  subfaclim  32560  kur14lem6  32583  quad3  33038  iexpire  33092  volsupnfl  35118  dfxrn2  35804  xrninxp  35816  ipiiie0  39589  sn-0tie0  39591  areaquad  40181  wallispilem4  42725  dirkertrigeqlem3  42757  dirkercncflem1  42760  fourierswlem  42887  fouriersw  42888  smflimsuplem8  43473  3exp4mod41  44149  41prothprm  44152  tgoldbachlt  44349  zlmodzxz0  44773  linevalexample  44818
 Copyright terms: Public domain W3C validator