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

Theorem 3eqtr2d 2334
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 2331 . 2  |-  ( ph  ->  A  =  C )
4 3eqtr2d.3 . 2  |-  ( ph  ->  C  =  D )
53, 4eqtrd 2328 1  |-  ( ph  ->  A  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  negsub  9111  neg2sub  9123  divmuleq  9481  divneg2  9500  discr  11254  bcpasc  11349  hashgval2  11376  hashf1lem2  11410  crim  11616  isum1p  12316  geo2sum  12345  efi4p  12433  sinhval  12450  addcos  12470  cos2tsin  12475  demoivreALT  12497  rpnnen2lem11  12519  sadaddlem  12673  smumullem  12699  sqgcd  12753  eulerthlem2  12866  omeo  12883  pockthlem  12968  4sqlem10  13010  vdwlem2  13045  vdwlem6  13049  vdwlem8  13051  fuccocl  13854  resssetc  13940  resscatc  13953  uncfcurf  14029  yonedalem3b  14069  prdspjmhm  14459  grpinvid2  14547  imasgrp2  14626  lagsubg2  14694  cntzsubm  14827  sylow3lem2  14955  efgredleme  15068  ablsubsub  15135  ablsubsub4  15136  odadd2  15157  gex2abl  15159  pgpfac1lem3a  15327  abvneg  15615  lsppr  15862  psrass1  16166  resspsradd  16176  resspsrvsca  16178  mplcoe2  16227  mplmon2mul  16258  evlslem2  16265  coe1tm  16365  ply1scl1  16383  gzrngunit  16453  cmpfi  17151  cnconn  17164  txrest  17341  blcvx  18320  tchcphlem2  18682  minveclem2  18806  pjthlem1  18817  uniioovol  18950  uniioombllem2  18954  itg1addlem4  19070  mbfi1fseqlem5  19090  itg2mulc  19118  itg2monolem1  19121  itgaddlem1  19193  itgmulc2lem2  19203  dvrec  19320  lhop2  19378  ftc1lem5  19403  deg1submon1p  19554  plypf1  19610  coefv0  19645  coemulhi  19651  coemulc  19652  dgreq0  19662  dvply1  19680  vieta1  19708  aareccl  19722  dvtaylp  19765  mtest  19797  sineq0  19905  efif1olem2  19921  efif1olem4  19923  tanarg  19986  logtayl2  20025  isosctrlem2  20135  chordthmlem2  20146  chordthmlem4  20148  dcubic1lem  20155  dcubic1  20157  mcubic  20159  dquart  20165  quart1lem  20167  quart1  20168  efiasin  20200  asinsin  20204  atancj  20222  efiatan  20224  atanlogaddlem  20225  cosatan  20233  atantan  20235  atans2  20243  log2cnv  20256  log2tlbnd  20257  birthdaylem2  20263  cxplim  20282  wilthlem1  20322  basellem3  20336  musum  20447  musumsum  20448  muinv  20449  pclogsum  20470  mersenne  20482  dchrabs  20515  dchrinv  20516  lgseisenlem1  20604  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2lem1  20613  chebbnd1lem3  20636  chpchtlim  20644  rplogsumlem2  20650  dchrisumlem2  20655  dchrmusum2  20659  mulog2sumlem1  20699  mulog2sumlem3  20701  vmalogdivsum2  20703  selberg4lem1  20725  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  pntibndlem2  20756  pntlemr  20767  pntlemf  20770  pntlemo  20772  grpoinvid2  20914  gxcom  20952  gxmodid  20962  ablodivdiv4  20974  vcoprne  21151  nvnncan  21237  smcnlem  21286  ipidsq  21302  ipasslem2  21426  minvecolem2  21470  hv2times  21656  pjhthlem1  21986  pjds3i  22308  ho2times  22415  opsqrlem6  22741  pjclem4  22795  pj3si  22803  csmdsymi  22930  ballotlemscr  23093  ballotlemfrci  23102  fmptapd  23228  ofoprabco  23247  nnlogbexp  23421  esumpr2  23454  esumpfinval  23458  esumpfinvalf  23459  orvcelval  23684  subfacp1lem5  23730  cvmliftlem10  23840  brbtwn2  24605  colinearalglem1  24606  colinearalglem2  24607  axcontlem2  24665  axcontlem8  24671  fsumkthpow  24863  bpoly3  24865  bpoly4  24866  itgaddnclem1  25009  itgmulc2nclem2  25018  areacirclem2  25028  areacirclem5  25032  mvecrtol2  25580  2wsms  25711  cmpmon  25918  istotbnd3  26598  iscringd  26727  diophin  26955  irrapxlem2  27011  pellexlem6  27022  pell1234qrmulcl  27043  rmxyval  27103  rmxyadd  27109  jm2.24  27153  jm2.25  27195  frlmgsum  27335  mamuass  27563  isumneg  27831  stoweidlem42  27894  sharhght  27958  sinhpcosh  28464  3atlem1  30294  pmod2iN  30660  polval2N  30717  lhple  30853  cdleme2  31039  cdleme35d  31263  cdleme42h  31293  cdlemeg46ngfr  31329  cdlemkid1  31733  lcfl7lem  32311  mapdpglem22  32505  mapdh6dN  32551  hdmap1l6d  32626  hdmapinvlem3  32735
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