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

Theorem 3eqtr2i 2679
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 2676 . 2 𝐴 = 𝐶
4 3eqtr2i.3 . 2 𝐶 = 𝐷
53, 4eqtri 2673 1 𝐴 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  indif  3902  dfrab3  3935  iunid  4607  cnvcnvOLD  5622  cocnvcnv2  5685  fmptap  6477  cnvoprab  7274  fpar  7326  fodomr  8152  jech9.3  8715  cda1dif  9036  alephadd  9437  distrnq  9821  ltanq  9831  ltrnq  9839  halfpm6th  11291  numma  11595  numaddc  11599  6p5lem  11633  8p2e10  11648  binom2i  13014  faclbnd4lem1  13120  cats2cat  13653  0.999...  14656  0.999...OLD  14657  flodddiv4  15184  6gcd4e2  15302  dfphi2  15526  mod2xnegi  15822  karatsuba  15839  karatsubaOLD  15840  1259lem1  15885  oppgtopn  17829  mgptopn  18544  ply1plusg  19643  ply1vsca  19644  ply1mulr  19645  restcld  21024  cmpsublem  21250  kgentopon  21389  txswaphmeolem  21655  dfii5  22735  itg1climres  23526  ang180lem1  24584  1cubrlem  24613  quart1lem  24627  efiatan  24684  log2cnv  24716  log2ublem3  24720  1sgm2ppw  24970  ppiub  24974  bposlem8  25061  bposlem9  25062  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  ax5seglem7  25860  2pthd  26905  3pthd  27152  ipidsq  27693  ipdirilem  27812  norm3difi  28132  polid2i  28142  pjclem3  29184  cvmdi  29311  indifundif  29482  dpmul  29749  eulerpartlemt  30561  eulerpart  30572  ballotlem1  30676  ballotlemfval0  30685  ballotth  30727  hgt750lem  30857  hgt750lem2  30858  subfaclim  31296  kur14lem6  31319  quad3  31690  iexpire  31747  pigt3  33532  volsupnfl  33584  dfxrn2  34278  xrninxp  34290  areaquad  38119  wallispilem4  40603  dirkertrigeqlem3  40635  dirkercncflem1  40638  fourierswlem  40765  fouriersw  40766  smflimsuplem8  41354  3exp4mod41  41858  41prothprm  41861  tgoldbachlt  42029  tgoldbachltOLD  42035  zlmodzxz0  42459  linevalexample  42509
  Copyright terms: Public domain W3C validator