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

Theorem 3eqtr4rd 2339
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
2 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2eqtr4d 2331 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2331 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  odi  6593  phplem4  7059  cantnfp1lem3  7398  cantnfp1  7399  cardidm  7608  ackbij2lem2  7882  ackbij2lem3  7883  divneg  9471  xadddilem  10630  xadddi2  10633  modlt  10997  modmulnn  11004  seqcaopr3  11097  bcval5  11346  hashgadd  11375  hashun3  11382  seqcoll  11417  revco  11505  cjreb  11624  recj  11625  imcj  11633  imval2  11652  sqrmul  11761  absmax  11829  amgm2  11869  summolem2a  12204  fsumf1o  12212  sumsn  12229  sumsplit  12247  fsummulc2  12262  binom  12304  bcxmas  12310  incexclem  12311  incexc  12312  expcnv  12338  cvgrat  12355  ege2le3  12387  efaddlem  12390  eftlub  12405  tanval3  12430  tanneg  12444  cosmul  12469  cos01bnd  12482  demoivreALT  12497  bitsp1  12638  absmulgcd  12742  eulerthlem2  12866  pythagtriplem14  12897  pcmul  12920  pcfac  12963  prmreclem6  12984  4sqlem12  13019  vdwlem6  13049  oppccatid  13638  curf2ndf  14037  oppcyon  14059  joincomALT  14151  meetcomALT  14153  pwsco1mhm  14462  mulgnn0p1  14594  mulgneg  14601  mulgnn0dir  14606  divsgrp2  14629  divsghm  14735  gaid  14769  odmulg  14885  sylow1lem2  14926  sylow2a  14946  sylow3lem1  14954  efgredleme  15068  efgcpbllemb  15080  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  lmodsubdi  15698  0lmhm  15813  lspsneq  15891  divsrhm  16005  divscrng  16008  asclrhm  16097  resspsrmul  16177  psropprmul  16332  zlpirlem3  16459  mulgrhm  16476  ptbasfi  17292  ptuni  17305  alexsubALTlem3  17759  subgtgp  17804  tsmsxplem1  17851  nminv  18158  nrginvrcnlem  18217  copco  18532  pcoass  18538  pi1bas  18552  pi1xfrf  18567  pi1xfr  18569  cph2subdi  18661  cphassr  18663  tchcphlem1  18681  pjthlem1  18817  ovolunlem1a  18871  ovolfs2  18942  uniiccdif  18949  ismbf  19001  itgaddlem2  19194  ditgswap  19225  ply1divex  19538  plyeq0lem  19608  plymullem1  19612  dgrcolem2  19671  vieta1lem2  19707  elqaalem2  19716  elqaalem3  19717  aaliou3lem7  19745  ulmshft  19785  mulcxplem  20047  cxpmul2  20052  root1eq1  20111  cxpeq  20113  cosangneg2d  20121  isosctrlem2  20135  angpieqvdlem  20141  chordthmlem3  20147  chordthmlem4  20148  chordthmlem5  20149  quad2  20151  dcubic2  20156  cubic2  20160  quart1  20168  scvxcvx  20296  basellem9  20342  ppifl  20414  mumul  20435  sgmmul  20456  chtublem  20466  chpub  20475  logfacrlim  20479  dchrsum2  20523  sumdchr2  20525  bposlem9  20547  lgsdir2  20583  lgsdir  20585  lgsdi  20587  lgsdirnn0  20594  lgsdinn0  20595  2sqblem  20632  chpo1ub  20645  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2if  20662  dchrisum0fmul  20671  rpvmasum2  20677  mulog2sumlem1  20699  vmalogdivsum2  20703  log2sumbnd  20709  selberg3lem1  20722  selberg4lem1  20725  pntrsumo1  20730  selbergr  20733  pntpbnd1  20751  pntlemk  20771  gxnn0suc  20947  gxinv  20953  vsfval  21207  lnocoi  21351  nmblolbii  21393  ipasslem5  21429  hvsubid  21621  sshjval3  21949  pjhthlem1  21986  adjval  22486  unopf1o  22512  kbpj  22552  lnopmi  22596  nmcoplbi  22624  cnlnadjlem2  22664  adjadd  22689  branmfn  22701  pjtoi  22775  ballotlemsf1o  23088  csbcnvg  23213  fimacnvinrn2  23215  ofoprabco  23247  xrsmulgzz  23322  xrge0iifhom  23334  xrge0adddir  23347  esumsn  23452  measvunilem0  23556  cvmlift3lem2  23866  cvmlift3lem4  23868  cvmlift3lem5  23869  cvmlift3lem6  23870  cvmlift3lem9  23873  faclimlem5  24121  prodmolem2a  24157  fprodf1o  24172  axlowdimlem16  24657  axcontlem8  24671  itgaddnclem2  25010  areacirclem6  25033  areacirc  25034  2wsms  25711  addassv  25759  upixp  26506  prdsbnd2  26622  ismrer1  26665  rngoneglmul  26685  rngoisocnv  26715  pellexlem2  27018  rmxyneg  27108  oddcomabszz  27132  acongeq  27173  psgnunilem2  27521  phisum  27621  hausgraph  27634  expgrowth  27655  sumsnd  27800  sigarperm  27953  reccot  28482  rectan  28483  cotsqcscsq  28486  islshpsm  29792  lshpnel2N  29797  lfl0f  29881  ldualvsdi1  29955  ldualgrplem  29957  cmtcomlemN  30060  cvlsupr8  30161  pmodl42N  30662  pmapjat1  30664  llnmod2i2  30674  dalawlem2  30683  pmapj2N  30740  idltrn  30961  cdlemc6  31007  cdleme20d  31123  cdleme22e  31155  cdleme22eALTN  31156  cdleme35b  31261  cdleme48fvg  31311  cdlemg4d  31424  cdlemg8a  31438  cdlemg42  31540  cdlemg47a  31545  tendodi1  31595  tendodi2  31596  cdlemk4  31645  cdlemk21N  31684  cdlemk22  31704  cdlemky  31737  cdlemk53b  31767  cdlemk53  31768  cdlemkyyN  31773  erngdvlem3-rN  31809  tendocnv  31833  dia1dim2  31874  dicvaddcl  32002  dihglblem3N  32107  dihmeetlem4preN  32118  dihmeet2  32158  lcfl7lem  32311  baerlem3lem1  32519  baerlem5alem1  32520  mapdh6bN  32549  mapdh6cN  32550  mapdh6dN  32551  hdmap1l6b  32624  hdmap1l6c  32625  hdmap1l6d  32626  hdmap14lem13  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator