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

Theorem 3eqtr2d 2321
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3eqtr2d.1  |-  ( ph  ->  A  =  B )
3eqtr2d.2  |-  ( ph  ->  C  =  B )
3eqtr2d.3  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
3eqtr2d  |-  ( ph  ->  A  =  D )

Proof of Theorem 3eqtr2d
StepHypRef Expression
1 3eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr2d.2 . . 3  |-  ( ph  ->  C  =  B )
31, 2eqtr4d 2318 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtrd 2315 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  negsub  9095  neg2sub  9107  divmuleq  9465  divneg2  9484  discr  11238  bcpasc  11333  hashgval2  11360  hashf1lem2  11394  crim  11600  isum1p  12300  geo2sum  12329  efi4p  12417  sinhval  12434  addcos  12454  cos2tsin  12459  demoivreALT  12481  rpnnen2lem11  12503  sadaddlem  12657  smumullem  12683  sqgcd  12737  eulerthlem2  12850  omeo  12867  pockthlem  12952  4sqlem10  12994  vdwlem2  13029  vdwlem6  13033  vdwlem8  13035  fuccocl  13838  resssetc  13924  resscatc  13937  uncfcurf  14013  yonedalem3b  14053  prdspjmhm  14443  grpinvid2  14531  imasgrp2  14610  lagsubg2  14678  cntzsubm  14811  sylow3lem2  14939  efgredleme  15052  ablsubsub  15119  ablsubsub4  15120  odadd2  15141  gex2abl  15143  pgpfac1lem3a  15311  abvneg  15599  lsppr  15846  psrass1  16150  resspsradd  16160  resspsrvsca  16162  mplcoe2  16211  mplmon2mul  16242  evlslem2  16249  coe1tm  16349  ply1scl1  16367  gzrngunit  16437  cmpfi  17135  cnconn  17148  txrest  17325  blcvx  18304  tchcphlem2  18666  minveclem2  18790  pjthlem1  18801  uniioovol  18934  uniioombllem2  18938  itg1addlem4  19054  mbfi1fseqlem5  19074  itg2mulc  19102  itg2monolem1  19105  itgaddlem1  19177  itgmulc2lem2  19187  dvrec  19304  lhop2  19362  ftc1lem5  19387  deg1submon1p  19538  plypf1  19594  coefv0  19629  coemulhi  19635  coemulc  19636  dgreq0  19646  dvply1  19664  vieta1  19692  aareccl  19706  dvtaylp  19749  mtest  19781  sineq0  19889  efif1olem2  19905  efif1olem4  19907  tanarg  19970  logtayl2  20009  isosctrlem2  20119  chordthmlem2  20130  chordthmlem4  20132  dcubic1lem  20139  dcubic1  20141  mcubic  20143  dquart  20149  quart1lem  20151  quart1  20152  efiasin  20184  asinsin  20188  atancj  20206  efiatan  20208  atanlogaddlem  20209  cosatan  20217  atantan  20219  atans2  20227  log2cnv  20240  log2tlbnd  20241  birthdaylem2  20247  cxplim  20266  wilthlem1  20306  basellem3  20320  musum  20431  musumsum  20432  muinv  20433  pclogsum  20454  mersenne  20466  dchrabs  20499  dchrinv  20500  lgseisenlem1  20588  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2lem1  20597  chebbnd1lem3  20620  chpchtlim  20628  rplogsumlem2  20634  dchrisumlem2  20639  dchrmusum2  20643  mulog2sumlem1  20683  mulog2sumlem3  20685  vmalogdivsum2  20687  selberg4lem1  20709  pntrlog2bndlem2  20727  pntrlog2bndlem4  20729  pntibndlem2  20740  pntlemr  20751  pntlemf  20754  pntlemo  20756  grpoinvid2  20898  gxcom  20936  gxmodid  20946  ablodivdiv4  20958  vcoprne  21135  nvnncan  21221  smcnlem  21270  ipidsq  21286  ipasslem2  21410  minvecolem2  21454  hv2times  21640  pjhthlem1  21970  pjds3i  22292  ho2times  22399  opsqrlem6  22725  pjclem4  22779  pj3si  22787  csmdsymi  22914  ballotlemscr  23077  ballotlemfrci  23086  fmptapd  23213  ofoprabco  23232  nnlogbexp  23406  esumpr2  23439  esumpfinval  23443  esumpfinvalf  23444  orvcelval  23669  subfacp1lem5  23715  cvmliftlem10  23825  brbtwn2  24533  colinearalglem1  24534  colinearalglem2  24535  axcontlem2  24593  axcontlem8  24599  fsumkthpow  24791  bpoly3  24793  bpoly4  24794  areacirclem2  24925  areacirclem5  24929  mvecrtol2  25477  2wsms  25608  cmpmon  25815  istotbnd3  26495  iscringd  26624  diophin  26852  irrapxlem2  26908  pellexlem6  26919  pell1234qrmulcl  26940  rmxyval  27000  rmxyadd  27006  jm2.24  27050  jm2.25  27092  frlmgsum  27232  mamuass  27460  isumneg  27728  stoweidlem42  27791  sharhght  27855  sinhpcosh  28210  3atlem1  29672  pmod2iN  30038  polval2N  30095  lhple  30231  cdleme2  30417  cdleme35d  30641  cdleme42h  30671  cdlemeg46ngfr  30707  cdlemkid1  31111  lcfl7lem  31689  mapdpglem22  31883  mapdh6dN  31929  hdmap1l6d  32004  hdmapinvlem3  32113
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