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

Theorem 3eqtr4a 2449
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1  |-  A  =  B
3eqtr4a.2  |-  ( ph  ->  C  =  A )
3eqtr4a.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3  |-  ( ph  ->  C  =  A )
2 3eqtr4a.1 . . 3  |-  A  =  B
31, 2syl6eq 2439 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2426 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374
This theorem is referenced by:  rabsnif  4013  uniintsn  4237  iinvdif  4315  iununi  4331  unizlim  4908  dmxpid  5135  rnxpid  5350  csbrn  5377  dmsnsnsn  5394  opswap  5403  xpcoid  5457  fvco4i  5852  fndmdifcom  5894  fmptsng  5994  fmptsnd  5995  csbov  6231  ordunisuc  6566  offres  6694  1stval2  6716  2ndval2  6717  cnvf1olem  6797  fparlem3  6801  fparlem4  6802  imacosupp  6858  seqomlem1  7033  ecovcom  7335  ecovass  7336  ecovdi  7337  resixpfo  7426  mapunen  7605  cardidm  8253  cardiun  8276  alephcard  8364  cardalephex  8384  cardcf  8545  cfidm  8568  alephsing  8569  itunisuc  8712  itunitc  8714  ituniiun  8715  alephadd  8865  alephreg  8870  pwcfsdom  8871  addcompq  9239  addcomnq  9240  mulcompq  9241  mulcomnq  9242  addassnq  9247  mulassnq  9248  addid1  9671  zeo  10865  xnegneg  11334  xaddcom  11358  xaddid1  11359  xnegdi  11361  xmulid1  11392  xadddilem  11407  ixxin  11467  fzsuc2  11659  expneg  12077  sq01  12190  facp1  12260  bcpasc  12301  hashf1lem1  12408  hashf1  12410  swrdccatin1  12619  swrdccat3blem  12631  repswsymballbi  12663  cshwmodn  12677  repswcshw  12691  trclun  12852  relexpcnv  12870  absexp  13139  sqreulem  13194  fsumf1o  13547  fsumadd  13563  fsumrev2  13599  fsumparts  13622  fsumrelem  13623  fprodf1o  13755  fprodmul  13767  fproddiv  13768  fprodfac  13779  efexp  13838  tanval2  13870  sqr2irrlem  13983  sadeq  14124  smumullem  14144  smumul  14145  gcdcom  14160  gcd0id  14163  gcdass  14185  nn0gcdsq  14287  dfphi2  14306  pcneg  14399  setscom  14666  strfvi  14676  setsnid  14678  ressbas  14691  ressinbas  14697  ressress  14699  firest  14840  topnval  14842  xpsfeq  14971  xpsaddlem  14982  xpsvsca  14986  homffval  15096  oppchomfval  15120  oppcbas  15124  rescbas  15235  rescco  15238  cofuass  15295  fucbas  15366  fuchom  15367  setccatid  15480  estrccatid  15518  xpcbas  15564  xpchomfval  15565  xpccofval  15568  oduleval  15878  oduglb  15886  odulub  15888  ipotset  15904  grpinvfvi  16208  cntrval  16474  cntzval  16476  oppgplusfval  16500  symgbas  16522  symggrp  16542  pmtrprfval  16629  m1expaddsub  16640  sylow1lem2  16736  sylow3lem1  16764  oppglsm  16779  gsumzsplit  17061  gsumzsplitOLD  17062  gsum2dlem2  17112  gsum2dOLD  17114  gsumcom2  17117  dprd2dlem2  17202  dprd2da  17204  dmdprdsplit2lem  17207  mgpplusg  17258  mgpress  17265  ringidval  17268  opprmulfval  17387  abvtrivd  17602  sralem  17936  srasca  17940  sravsca  17941  sraip  17942  rlmval  17950  psrmulr  18150  mplmonmul  18239  mplcoe3  18241  mplcoe3OLD  18242  opsrbaslem  18255  opsrtoslem2  18262  psr1val  18338  ply1basfvi  18395  ply1plusgfvi  18396  psr1sca2  18405  evl1fval1lem  18479  zlmlem  18647  zlmsca  18651  zlmvsca  18652  psgninv  18709  ocvval  18789  thlbas  18818  thlle  18819  thloc  18821  dsmmval2  18858  mattpos1  19043  mdettpos  19198  smadiadetglem1  19258  tgdif0  19579  indislem  19586  restco  19751  txtopon  20177  txindislem  20219  qtopres  20284  hmphindis  20383  ptuncnv  20393  snclseqg  20699  tsmssplit  20739  ussval  20847  tuslem  20855  setsmsbas  21063  tnglem  21239  tngds  21247  tngtset  21248  pcoass  21609  cphsqrtcl2  21718  rrxcph  21909  ovolunlem1a  21992  ioorinv  22070  itg11  22183  itg1mulc  22196  itg2cnlem1  22253  iblss2  22297  ibladdlem  22311  itgfsum  22318  iblabslem  22319  iblabs  22320  ditgneg  22346  deg1fvi  22570  dgrco  22757  logfac  23073  cxpexp  23136  cxpmul2  23157  cxpsqrt  23171  dvcxp1  23203  dvcxp2  23204  ang180lem1  23259  mcubic  23294  quart1  23303  reasinsin  23343  atanlogaddlem  23360  atantayl2  23385  log2tlbnd  23392  basellem2  23472  basellem3  23473  basellem5  23475  basellem8  23478  dchrmulid2  23644  bcp1ctr  23671  lgsneg  23711  lgsneg1  23712  lgsdir2  23720  lgsdir  23722  lgsdi  23724  lgsquad2lem2  23751  pntleml  23913  motgrp  24050  lmiisolem  24281  ttglem  24300  eupath2lem3  25100  bafval  25614  ipidsq  25740  ipasslem1  25863  pjclem2  27231  cvmdi  27359  imadifxp  27591  iundisjcnt  27756  resvsca  27974  indval2  28163  bayesth  28561  plymulx  28688  subfacp1lem6  28818  mvtval  29049  mexval  29051  mexval2  29052  mdvval  29053  mrsubfval  29057  mrsubvrs  29071  msubfval  29073  elmsubrn  29077  mvhfval  29082  mpstval  29084  msrfval  29086  mstaval  29093  mthmval  29124  fallfacfwd  29324  dfrdg2  29393  dfrdg3  29394  dfrdg4  29753  ordtoplem  30053  ordcmp  30065  mblfinlem2  30217  itg2addnclem2  30233  ibladdnclem  30237  iblabsnclem  30244  iblabsnc  30245  iblmulc2nc  30246  ftc1anclem8  30263  kelac2  31177  mendbas  31301  mendsca  31306  mendring  31309  lcmcom  31367  lcmneg  31377  lcmass  31386  iotain  31492  addrcom  31552  itgsinexplem1  31918  volioc  31937  dirkertrigeqlem1  32046  fourierdlem104  32159  sqwvfoura  32177  sqwvfourb  32178  rngccatidALTV  32997  ringccatidALTV  33060  0dig2pr01  33431  nn0sumshdiglemB  33441  dpfrac1  33502  pmodN  35987  tgrpgrplem  36888  tendoplass  36922  tendoicl  36935  erngdvlem3  37129  dvhvaddass  37237  dib0  37304  dib1dim2  37308  diclspsn  37334  cdlemn8  37344  dihopelvalcpre  37388  djhcom  37545  relexpaddss  38223  relexp01min  38237
  Copyright terms: Public domain W3C validator