MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr3i Unicode version

Theorem 3eqtr3i 2311
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3i.1  |-  A  =  B
3eqtr3i.2  |-  A  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3i  |-  C  =  D

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3  |-  A  =  B
2 3eqtr3i.2 . . 3  |-  A  =  C
31, 2eqtr3i 2305 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2305 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  csbvarg  3108  un12  3333  in12  3380  indif1  3413  difundi  3421  difundir  3422  difindi  3423  difindir  3424  dif32  3431  undif1  3529  orduniss2  4624  resmpt3  5001  xp0  5098  fresaunres2  5413  fvsnun1  5715  caov12  6048  caov13  6050  caov411  6052  caovdir  6054  fparlem3  6220  fparlem4  6221  hartogslem1  7257  kmlem3  7778  cdaassen  7808  xpcdaen  7809  halfnq  8600  reclem3pr  8673  addcmpblnr  8694  ltsrpr  8699  pn0sr  8723  sqgt0sr  8728  map2psrpr  8732  negsubdii  9131  halfpm6th  9936  i4  11205  nn0opthlem1  11283  fac4  11296  imi  11642  ef01bndlem  12464  bitsres  12664  gcdaddmlem  12707  modsubi  13087  gcdmodi  13089  numexpp1  13093  karatsuba  13099  oppgcntr  14838  frgpuplem  15081  ressmpladd  16201  ressmplmul  16202  ressmplvsca  16203  ltbwe  16214  ressply1add  16308  ressply1mul  16309  ressply1vsca  16310  sn0cld  16827  qtopres  17389  itg1addlem5  19055  cospi  19840  sincos4thpi  19881  sincos3rdpi  19884  dvlog  19998  dvlog2  20000  dvsqr  20084  ang180lem3  20109  1cubrlem  20137  mcubic  20143  quart1lem  20151  atantayl2  20234  log2cnv  20240  log2ublem2  20243  log2ub  20245  chtub  20451  bclbnd  20519  bposlem8  20530  lgsdir2lem1  20562  lgsdir2lem5  20566  ipidsq  21286  ip1ilem  21404  ipdirilem  21407  ipasslem10  21417  siilem1  21429  hvmul2negi  21627  hvadd12i  21636  hvnegdii  21641  normlem1  21689  normlem9  21697  normsubi  21720  normpar2i  21735  polid2i  21736  chjassi  22065  chj12i  22101  pjoml2i  22164  hoadd12i  22357  lnophmlem2  22597  nmopcoadj2i  22682  sqsscirc1  23292  sigaclfu2  23482  coinflippvt  23685  bpoly3  24793  onint1  24888  rabren3dioph  26898  lhe4.4ex1a  27546  expgrowthi  27550  expgrowth  27552
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator