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

Theorem 3eqtr3rd 2479
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
2 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
3 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
42, 3eqtr3d 2472 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2472 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431
This theorem is referenced by:  fcofo  5987  fcof1o  5992  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  fin1a2lem7  8567  prlem934  9194  addid2  9544  addcom  9547  addcomd  9563  negeu  9592  add20  9843  2halves  10545  bcnn  12080  bcpasc  12089  hashfun  12191  wrdeqs1cat  12361  sqreulem  12839  summolem3  13183  fsumneg  13246  geolim  13322  geolim2  13323  mertens  13338  sincossq  13452  demoivre  13476  eirrlem  13478  sadeq  13660  gcdid  13707  phiprmpw  13843  pythagtriplem12  13885  expnprm  13956  fullresc  14753  grpinvid1  15577  grpnpcan  15608  grplactcnv  15615  conjghm  15768  odmodnn0  16034  gex1  16081  sylow3lem3  16119  efgredeu  16240  odadd2  16322  gsumval3OLD  16373  gsumval3  16376  pgpfac1lem3a  16565  rngnegl  16673  rngnegr  16674  rngmneg2  16676  lmodvsneg  16967  lss0v  17074  lssvs0or  17168  lvecinv  17171  lspabs2  17178  mplcoe3  17522  mplcoe3OLD  17523  mplcoe2  17524  mplcoe2OLD  17525  evlvar  17590  zringcyg  17882  zcyg  17887  zringunit  17889  zrngunit  17890  mdetrlin  18384  mdetunilem6  18398  cramerimplem3  18466  cramerimp  18467  paste  18873  tuslem  19817  tususs  19820  ngpds  20170  ioo2bl  20345  ipcau2  20724  cmetcusp  20841  dvexp3  21425  rolle  21437  cmvth  21438  dv11cn  21448  lhop  21463  itgsubstlem  21495  ply1divex  21583  fta1glem1  21612  fta1g  21614  fta1  21749  vieta1lem2  21752  aaliou2  21781  dvtaylp  21810  dvntaylp  21811  taylthlem1  21813  taylthlem2  21814  dvradcnv  21861  ptolemy  21933  coskpi  21957  tanregt0  21970  cxpeq  22170  isosctrlem2  22192  chordthmlem  22202  dcubic  22216  quart1lem  22225  tanatan  22289  atantan  22293  dvatan  22305  birthdaylem2  22321  rlimcxp  22342  jensenlem2  22356  logdiflbnd  22363  emcllem2  22365  basellem8  22400  bclbnd  22594  lgsqr  22660  lgseisenlem3  22665  lgseisenlem4  22666  lgsquadlem1  22668  lgsquadlem2  22669  rpvmasumlem  22711  dchrisumlem1  22713  dchrisum0flblem1  22732  dchrisum0flblem2  22733  dchrisum0re  22737  dchrisum0lem1  22740  mudivsum  22754  mulogsum  22756  vmalogdivsum2  22762  logsqvma2  22767  selberg2lem  22774  logdivbnd  22780  selbergr  22792  selberg3r  22793  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  pntpbnd2  22811  miduniq2  23046  krippenlem  23049  ttgcontlem1  23082  brbtwn2  23102  colinearalglem4  23106  axsegconlem9  23122  ax5seglem1  23125  axbtwnid  23136  axeuclidlem  23159  axcontlem2  23162  axcontlem4  23164  grpoinvid1  23668  vcz  23899  hosubsub4  25173  lnop0  25321  branmfn  25460  difico  26024  omndmul2  26126  rdivmuldivd  26210  kerunit  26242  ballotlemfrceq  26863  ballotlemrinv0  26867  wrdsplex  26891  lgamgulmlem2  26968  lgamcvg2  26993  prodmolem3  27397  fallrisefac  27479  faclimlem1  27500  bpoly3  28152  mblfinlem2  28382  voliunnfl  28388  volsupnfl  28389  itg2addnclem3  28398  ftc2nc  28429  dvasin  28433  areacirclem1  28437  areacirclem4  28440  rngonegmn1l  28708  rngonegmn1r  28709  irrapxlem5  29120  pellfund14  29192  rmxdbl  29233  jm2.22  29297  dgrnznn  29445  itgpowd  29543  sigariz  29852  clwwlkel  30408  altgsumbc  30700  lfl0  32550  latmassOLD  32714  omlmod1i2N  32745  llnexchb2lem  33352  dalawlem3  33357  pmapj2N  33413  osumcllem9N  33448  pexmidlem6N  33459  4atexlemc  33553  cdleme1  33711  cdleme42a  33955  cdlemg13a  34135  cdlemh2  34300  cdlemk1  34315  tendocnv  34506  dihmeetlem12N  34803  dihmeetlem16N  34807  dihmeetlem19N  34810  dochsatshp  34936  dochexmidlem6  34950  mapdval4N  35117  mapdpglem28  35186  mapdpglem31  35188  mapdindp4  35208  hdmap14lem1a  35354  hdmapinvlem4  35409
  Copyright terms: Public domain W3C validator