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

Theorem 3eqtr4rd 2326
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 2318 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2318 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  odi  6577  phplem4  7043  cantnfp1lem3  7382  cantnfp1  7383  cardidm  7592  ackbij2lem2  7866  ackbij2lem3  7867  divneg  9455  xadddilem  10614  xadddi2  10617  modlt  10981  modmulnn  10988  seqcaopr3  11081  bcval5  11330  hashgadd  11359  hashun3  11366  seqcoll  11401  revco  11489  cjreb  11608  recj  11609  imcj  11617  imval2  11636  sqrmul  11745  absmax  11813  amgm2  11853  summolem2a  12188  fsumf1o  12196  sumsn  12213  sumsplit  12231  fsummulc2  12246  binom  12288  bcxmas  12294  incexclem  12295  incexc  12296  expcnv  12322  cvgrat  12339  ege2le3  12371  efaddlem  12374  eftlub  12389  tanval3  12414  tanneg  12428  cosmul  12453  cos01bnd  12466  demoivreALT  12481  bitsp1  12622  absmulgcd  12726  eulerthlem2  12850  pythagtriplem14  12881  pcmul  12904  pcfac  12947  prmreclem6  12968  4sqlem12  13003  vdwlem6  13033  oppccatid  13622  curf2ndf  14021  oppcyon  14043  joincomALT  14135  meetcomALT  14137  pwsco1mhm  14446  mulgnn0p1  14578  mulgneg  14585  mulgnn0dir  14590  divsgrp2  14613  divsghm  14719  gaid  14753  odmulg  14869  sylow1lem2  14910  sylow2a  14930  sylow3lem1  14938  efgredleme  15052  efgcpbllemb  15064  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  lmodsubdi  15682  0lmhm  15797  lspsneq  15875  divsrhm  15989  divscrng  15992  asclrhm  16081  resspsrmul  16161  psropprmul  16316  zlpirlem3  16443  mulgrhm  16460  ptbasfi  17276  ptuni  17289  alexsubALTlem3  17743  subgtgp  17788  tsmsxplem1  17835  nminv  18142  nrginvrcnlem  18201  copco  18516  pcoass  18522  pi1bas  18536  pi1xfrf  18551  pi1xfr  18553  cph2subdi  18645  cphassr  18647  tchcphlem1  18665  pjthlem1  18801  ovolunlem1a  18855  ovolfs2  18926  uniiccdif  18933  ismbf  18985  itgaddlem2  19178  ditgswap  19209  ply1divex  19522  plyeq0lem  19592  plymullem1  19596  dgrcolem2  19655  vieta1lem2  19691  elqaalem2  19700  elqaalem3  19701  aaliou3lem7  19729  ulmshft  19769  mulcxplem  20031  cxpmul2  20036  root1eq1  20095  cxpeq  20097  cosangneg2d  20105  isosctrlem2  20119  angpieqvdlem  20125  chordthmlem3  20131  chordthmlem4  20132  chordthmlem5  20133  quad2  20135  dcubic2  20140  cubic2  20144  quart1  20152  scvxcvx  20280  basellem9  20326  ppifl  20398  mumul  20419  sgmmul  20440  chtublem  20450  chpub  20459  logfacrlim  20463  dchrsum2  20507  sumdchr2  20509  bposlem9  20531  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsdirnn0  20578  lgsdinn0  20579  2sqblem  20616  chpo1ub  20629  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2if  20646  dchrisum0fmul  20655  rpvmasum2  20661  mulog2sumlem1  20683  vmalogdivsum2  20687  log2sumbnd  20693  selberg3lem1  20706  selberg4lem1  20709  pntrsumo1  20714  selbergr  20717  pntpbnd1  20735  pntlemk  20755  gxnn0suc  20931  gxinv  20937  vsfval  21191  lnocoi  21335  nmblolbii  21377  ipasslem5  21413  hvsubid  21605  sshjval3  21933  pjhthlem1  21970  adjval  22470  unopf1o  22496  kbpj  22536  lnopmi  22580  nmcoplbi  22608  cnlnadjlem2  22648  adjadd  22673  branmfn  22685  pjtoi  22759  ballotlemsf1o  23072  csbcnvg  23198  fimacnvinrn2  23200  ofoprabco  23232  xrsmulgzz  23307  xrge0iifhom  23319  xrge0adddir  23332  esumsn  23437  measvunilem0  23541  cvmlift3lem2  23851  cvmlift3lem4  23853  cvmlift3lem5  23854  cvmlift3lem6  23855  cvmlift3lem9  23858  axlowdimlem16  24585  axcontlem8  24599  areacirclem6  24930  areacirc  24931  2wsms  25608  addassv  25656  upixp  26403  prdsbnd2  26519  ismrer1  26562  rngoneglmul  26582  rngoisocnv  26612  pellexlem2  26915  rmxyneg  27005  oddcomabszz  27029  acongeq  27070  psgnunilem2  27418  phisum  27518  hausgraph  27531  expgrowth  27552  sumsnd  27697  sigarperm  27850  reccot  28228  rectan  28229  cotsqcscsq  28232  islshpsm  29170  lshpnel2N  29175  lfl0f  29259  ldualvsdi1  29333  ldualgrplem  29335  cmtcomlemN  29438  cvlsupr8  29539  pmodl42N  30040  pmapjat1  30042  llnmod2i2  30052  dalawlem2  30061  pmapj2N  30118  idltrn  30339  cdlemc6  30385  cdleme20d  30501  cdleme22e  30533  cdleme22eALTN  30534  cdleme35b  30639  cdleme48fvg  30689  cdlemg4d  30802  cdlemg8a  30816  cdlemg42  30918  cdlemg47a  30923  tendodi1  30973  tendodi2  30974  cdlemk4  31023  cdlemk21N  31062  cdlemk22  31082  cdlemky  31115  cdlemk53b  31145  cdlemk53  31146  cdlemkyyN  31151  erngdvlem3-rN  31187  tendocnv  31211  dia1dim2  31252  dicvaddcl  31380  dihglblem3N  31485  dihmeetlem4preN  31496  dihmeet2  31536  lcfl7lem  31689  baerlem3lem1  31897  baerlem5alem1  31898  mapdh6bN  31927  mapdh6cN  31928  mapdh6dN  31929  hdmap1l6b  32002  hdmap1l6c  32003  hdmap1l6d  32004  hdmap14lem13  32073
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