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

Theorem 3eqtr4rd 2432
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 2424 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2424 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  odi  6760  phplem4  7227  cantnfp1lem3  7571  cantnfp1  7572  cardidm  7781  ackbij2lem2  8055  ackbij2lem3  8056  divneg  9643  xadddilem  10807  xadddi2  10810  modlt  11187  modmulnn  11194  seqcaopr3  11287  bcval5  11538  hashgadd  11580  hashun3  11587  seqcoll  11641  revco  11732  cjreb  11857  recj  11858  imcj  11866  imval2  11885  sqrmul  11994  absmax  12062  amgm2  12102  summolem2a  12438  fsumf1o  12446  sumsn  12463  sumsplit  12481  fsummulc2  12496  binom  12538  bcxmas  12544  incexclem  12545  incexc  12546  expcnv  12572  cvgrat  12589  ege2le3  12621  efaddlem  12624  eftlub  12639  tanval3  12664  tanneg  12678  cosmul  12703  cos01bnd  12716  demoivreALT  12731  absmulgcd  12976  eulerthlem2  13100  pythagtriplem14  13131  pcmul  13154  pcfac  13197  prmreclem6  13218  4sqlem12  13253  vdwlem6  13283  oppccatid  13874  curf2ndf  14273  oppcyon  14295  joincomALT  14387  meetcomALT  14389  pwsco1mhm  14698  mulgnn0p1  14830  mulgneg  14837  mulgnn0dir  14842  divsgrp2  14865  divsghm  14971  gaid  15005  odmulg  15121  sylow1lem2  15162  sylow2a  15182  sylow3lem1  15190  efgredleme  15304  efgcpbllemb  15316  gsumzaddlem  15455  gsumconst  15461  gsumzmhm  15462  lmodsubdi  15930  0lmhm  16045  lspsneq  16123  divsrhm  16237  divscrng  16240  asclrhm  16329  resspsrmul  16409  psropprmul  16561  zlpirlem3  16695  mulgrhm  16712  ptbasfi  17536  ptuni  17549  alexsubALTlem3  18003  subgtgp  18058  tsmsxplem1  18105  xmsusp  18490  restmetu  18491  nminv  18540  nrginvrcnlem  18599  copco  18916  pcoass  18922  pi1bas  18936  pi1xfrf  18951  pi1xfr  18953  cph2subdi  19045  cphassr  19047  tchcphlem1  19065  pjthlem1  19207  ovolunlem1a  19261  ovolfs2  19332  uniiccdif  19339  ismbf  19391  itgaddlem2  19584  ditgswap  19615  ply1divex  19928  plyeq0lem  19998  plymullem1  20002  dgrcolem2  20061  vieta1lem2  20097  elqaalem2  20106  elqaalem3  20107  aaliou3lem7  20135  ulmshft  20175  mulcxplem  20444  cxpmul2  20449  root1eq1  20508  cxpeq  20510  cosangneg2d  20518  isosctrlem2  20532  angpieqvdlem  20538  chordthmlem3  20544  chordthmlem4  20545  chordthmlem5  20546  quad2  20548  dcubic2  20553  cubic2  20557  quart1  20565  scvxcvx  20693  basellem9  20740  ppifl  20812  mumul  20833  sgmmul  20854  chtublem  20864  chpub  20873  logfacrlim  20877  dchrsum2  20921  sumdchr2  20923  bposlem9  20945  lgsdir2  20981  lgsdir  20983  lgsdi  20985  lgsdirnn0  20992  lgsdinn0  20993  2sqblem  21030  chpo1ub  21043  dchrmusum2  21057  dchrvmasumlem1  21058  dchrvmasum2if  21060  dchrisum0fmul  21069  rpvmasum2  21075  mulog2sumlem1  21097  vmalogdivsum2  21101  log2sumbnd  21107  selberg3lem1  21120  selberg4lem1  21123  pntrsumo1  21128  selbergr  21131  pntpbnd1  21149  pntlemk  21169  gxnn0suc  21702  gxinv  21708  vsfval  21964  lnocoi  22108  nmblolbii  22150  ipasslem5  22186  hvsubid  22378  sshjval3  22706  pjhthlem1  22743  adjval  23243  unopf1o  23269  kbpj  23309  lnopmi  23353  nmcoplbi  23381  cnlnadjlem2  23421  adjadd  23446  branmfn  23458  pjtoi  23532  csbcnvg  23882  fimacnvinrn2  23893  ofoprabco  23923  xrsmulgzz  24035  rdivmuldivd  24058  xrge0iifhom  24129  qqhval2lem  24166  qqhrhm  24174  esumsn  24254  measvunilem0  24363  ballotlemsf1o  24552  igamlgam  24615  lgam1  24629  cvmlift3lem2  24788  cvmlift3lem4  24790  cvmlift3lem5  24791  cvmlift3lem6  24792  cvmlift3lem9  24795  prodmolem3  25040  prodmolem2a  25041  fprodf1o  25053  prodsn  25067  fprodabs  25078  axlowdimlem16  25612  axcontlem8  25626  itgaddnclem2  25966  areacirclem6  25989  areacirc  25990  upixp  26124  prdsbnd2  26197  ismrer1  26240  rngoneglmul  26260  rngoisocnv  26290  pellexlem2  26586  rmxyneg  26676  oddcomabszz  26700  acongeq  26741  psgnunilem2  27089  phisum  27189  hausgraph  27202  expgrowth  27223  sumsnd  27367  fmuldfeqlem1  27382  cncfmptss  27387  climexp  27401  stoweidlem17  27436  wallispi  27489  sigarperm  27520  reccot  27849  rectan  27850  cotsqcscsq  27853  islshpsm  29097  lshpnel2N  29102  lfl0f  29186  ldualvsdi1  29260  ldualgrplem  29262  cmtcomlemN  29365  cvlsupr8  29466  pmodl42N  29967  pmapjat1  29969  llnmod2i2  29979  dalawlem2  29988  pmapj2N  30045  idltrn  30266  cdlemc6  30312  cdleme20d  30428  cdleme22e  30460  cdleme22eALTN  30461  cdleme35b  30566  cdleme48fvg  30616  cdlemg4d  30729  cdlemg8a  30743  cdlemg42  30845  cdlemg47a  30850  tendodi1  30900  tendodi2  30901  cdlemk4  30950  cdlemk21N  30989  cdlemk22  31009  cdlemky  31042  cdlemk53b  31072  cdlemk53  31073  cdlemkyyN  31078  erngdvlem3-rN  31114  tendocnv  31138  dia1dim2  31179  dicvaddcl  31307  dihglblem3N  31412  dihmeetlem4preN  31423  dihmeet2  31463  lcfl7lem  31616  baerlem3lem1  31824  baerlem5alem1  31825  mapdh6bN  31854  mapdh6cN  31855  mapdh6dN  31856  hdmap1l6b  31929  hdmap1l6c  31930  hdmap1l6d  31931  hdmap14lem13  32000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2382
  Copyright terms: Public domain W3C validator