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

Theorem 3eqtr3i 2651
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 𝐴 = 𝐵
3eqtr3i.2 𝐴 = 𝐶
3eqtr3i.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3i 𝐶 = 𝐷

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3 𝐴 = 𝐵
2 3eqtr3i.2 . . 3 𝐴 = 𝐶
31, 2eqtr3i 2645 . 2 𝐵 = 𝐶
4 3eqtr3i.3 . 2 𝐵 = 𝐷
53, 4eqtr3i 2645 1 𝐶 = 𝐷
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614
This theorem is referenced by:  un12  3755  in12  3808  indif1  3853  difundi  3861  difundir  3862  difindi  3863  difindir  3864  dif32  3873  csbvarg  3981  undif1  4021  resmpt3  5419  xp0  5521  fresaunres2  6043  fvsnun1  6413  caov12  6827  caov13  6829  caov411  6831  caovdir  6833  orduniss2  6995  fparlem3  7239  fparlem4  7240  hartogslem1  8407  kmlem3  8934  cdaassen  8964  xpcdaen  8965  halfnq  9758  reclem3pr  9831  addcmpblnr  9850  ltsrpr  9858  pn0sr  9882  sqgt0sr  9887  map2psrpr  9891  negsubdii  10326  halfpm6th  11213  decmul1  11545  i4  12923  nn0opthlem1  13011  fac4  13024  imi  13847  bpoly3  14733  ef01bndlem  14858  bitsres  15138  gcdaddmlem  15188  modsubi  15719  gcdmodi  15721  numexpp1  15725  karatsuba  15735  karatsubaOLD  15736  oppgcntr  17735  frgpuplem  18125  ressmpladd  19397  ressmplmul  19398  ressmplvsca  19399  ltbwe  19412  ressply1add  19540  ressply1mul  19541  ressply1vsca  19542  sn0cld  20834  qtopres  21441  itg1addlem5  23407  cospi  24162  sincos4thpi  24203  sincos3rdpi  24206  dvlog  24331  dvlog2  24333  dvsqrt  24417  dvcnsqrt  24419  ang180lem3  24475  1cubrlem  24502  mcubic  24508  quart1lem  24516  atantayl2  24599  log2cnv  24605  log2ublem2  24608  log2ub  24610  gam1  24725  chtub  24871  bclbnd  24939  bposlem8  24950  lgsdir2lem1  24984  lgsdir2lem5  24988  2lgsoddprmlem3d  25072  ex-bc  27197  ex-gcd  27202  ipidsq  27453  ip1ilem  27569  ipdirilem  27572  ipasslem10  27582  siilem1  27594  hvmul2negi  27793  hvadd12i  27802  hvnegdii  27807  normlem1  27855  normlem9  27863  normsubi  27886  normpar2i  27901  polid2i  27902  chjassi  28233  chj12i  28269  pjoml2i  28332  hoadd12i  28524  lnophmlem2  28764  nmopcoadj2i  28849  indifundif  29244  aciunf1  29346  partfun  29359  ffsrn  29388  archirngz  29570  sqsscirc1  29778  sigaclfu2  30007  eulerpartlemd  30251  coinflippvt  30369  ballotth  30422  quad3  31325  onint1  32143  bj-csbsn  32599  cnambfre  33129  rabren3dioph  36898  arearect  37321  areaquad  37322  resnonrel  37418  cononrel1  37420  cononrel2  37421  lhe4.4ex1a  38049  expgrowthi  38053  expgrowth  38055  binomcxplemnotnn0  38076  dvcosre  39461  stoweidlem34  39588  fouriersw  39785
  Copyright terms: Public domain W3C validator