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

Theorem 3eqtr4a 2534
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 2524 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2511 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  rabsnif  4096  uniintsn  4319  iinvdif  4397  iununi  4410  unizlim  4994  dmxpid  5221  rnxpid  5439  csbrn  5467  dmsnsnsn  5485  opswap  5494  xpcoid  5547  fvco4i  5944  fndmdifcom  5985  fmptsng  6081  fmptsnd  6082  csbov  6315  ordunisuc  6646  offres  6779  1stval2  6801  2ndval2  6802  cnvf1olem  6881  fparlem3  6885  fparlem4  6886  imacosupp  6940  seqomlem1  7115  ecovcom  7417  ecovass  7418  ecovdi  7419  resixpfo  7507  mapunen  7686  cardidm  8339  cardiun  8362  alephcard  8450  cardalephex  8470  cardcf  8631  cfidm  8654  alephsing  8655  itunisuc  8798  itunitc  8800  ituniiun  8801  alephadd  8951  alephreg  8956  pwcfsdom  8957  addcompq  9327  addcomnq  9328  mulcompq  9329  mulcomnq  9330  addassnq  9335  mulassnq  9336  addid1  9758  zeo  10945  xnegneg  11412  xaddcom  11436  xaddid1  11437  xnegdi  11439  xmulid1  11470  xadddilem  11485  ixxin  11545  fzsuc2  11736  expneg  12141  sq01  12255  facp1  12325  bcpasc  12366  hashf1lem1  12469  hashf1  12471  eqs1  12583  swrdccatin1  12670  swrdccat3blem  12682  repswsymballbi  12714  cshwmodn  12728  repswcshw  12742  absexp  13099  sqreulem  13154  fsumf1o  13507  fsumadd  13523  fsumrev2  13559  fsumparts  13582  fsumrelem  13583  efexp  13696  tanval2  13728  sqr2irrlem  13841  sadeq  13980  smumullem  14000  smumul  14001  gcdcom  14016  gcd0id  14019  gcdass  14041  nn0gcdsq  14143  dfphi2  14162  pcneg  14255  setscom  14519  strfvi  14529  setsnid  14531  ressbas  14544  ressinbas  14550  ressress  14551  firest  14687  topnval  14689  xpsfeq  14818  xpsaddlem  14829  xpsvsca  14833  homffval  14946  oppchomfval  14969  oppcbas  14973  rescbas  15058  rescco  15061  cofuass  15115  fucbas  15186  fuchom  15187  setccatid  15268  xpcbas  15304  xpchomfval  15305  xpccofval  15308  oduleval  15617  oduglb  15625  odulub  15627  ipotset  15643  grpinvfvi  15898  cntrval  16159  cntzval  16161  oppgplusfval  16185  symgbas  16207  symggrp  16227  pmtrprfval  16315  m1expaddsub  16326  sylow1lem2  16422  sylow3lem1  16450  oppglsm  16465  gsumzsplit  16744  gsumzsplitOLD  16745  gsum2dlem2  16798  gsum2dOLD  16800  gsumcom2  16803  dprd2dlem2  16888  dprd2da  16890  dmdprdsplit2lem  16893  mgpplusg  16944  mgpress  16951  rngidval  16954  opprmulfval  17070  abvtrivd  17284  sralem  17618  srasca  17622  sravsca  17623  sraip  17624  rlmval  17632  psrmulr  17824  mplmonmul  17913  mplcoe3  17915  mplcoe3OLD  17916  opsrbaslem  17929  opsrtoslem2  17936  psr1val  18012  ply1basfvi  18069  ply1plusgfvi  18070  psr1sca2  18079  evl1fval1lem  18153  zlmlem  18337  zlmsca  18341  zlmvsca  18342  psgninv  18401  ocvval  18481  thlbas  18510  thlle  18511  thloc  18513  dsmmval2  18550  mattpos1  18741  mdettpos  18896  smadiadetglem1  18956  tgdif0  19276  indislem  19283  restco  19447  txtopon  19843  txindislem  19885  qtopres  19950  hmphindis  20049  ptuncnv  20059  snclseqg  20365  tsmssplit  20405  ussval  20513  tuslem  20521  setsmsbas  20729  tnglem  20905  tngds  20913  tngtset  20914  pcoass  21275  cphsqrtcl2  21384  rrxcph  21575  ovolunlem1a  21658  ioorinv  21736  itg11  21849  itg1mulc  21862  itg2cnlem1  21919  iblss2  21963  ibladdlem  21977  itgfsum  21984  iblabslem  21985  iblabs  21986  ditgneg  22012  deg1fvi  22236  dgrco  22422  logfac  22729  cxpexp  22793  cxpmul2  22814  cxpsqrt  22828  dvcxp2  22861  ang180lem1  22885  mcubic  22922  quart1  22931  reasinsin  22971  atanlogaddlem  22988  atantayl2  23013  log2tlbnd  23020  basellem2  23099  basellem3  23100  basellem5  23102  basellem8  23105  dchrmulid2  23271  bcp1ctr  23298  lgsneg  23338  lgsneg1  23339  lgsdir2  23347  lgsdir  23349  lgsdi  23351  lgsquad2lem2  23378  pntleml  23540  motgrp  23674  ttglem  23871  eupath2lem3  24671  bafval  25189  ipidsq  25315  ipasslem1  25438  pjclem2  26807  cvmdi  26935  imadifxp  27147  iundisjcnt  27287  resvsca  27499  indval2  27684  bayesth  28034  subfacp1lem6  28285  fprodf1o  28671  fprodmul  28683  fproddiv  28684  fprodfac  28695  fallfacfwd  28751  dfrdg2  28821  dfrdg3  28822  dfrdg4  29193  ordtoplem  29493  ordcmp  29505  mblfinlem2  29645  itg2addnclem2  29660  ibladdnclem  29664  iblabsnclem  29671  iblabsnc  29672  iblmulc2nc  29673  ftc1anclem8  29690  kelac2  30631  mendbas  30754  mendsca  30759  mendrng  30762  lcmcom  30815  lcmneg  30825  lcmass  30834  iotain  30918  addrcom  30978  itgsinexplem1  31287  dpfrac1  32256  pmodN  34655  tgrpgrplem  35554  tendoplass  35588  tendoicl  35601  erngdvlem3  35795  dvhvaddass  35903  dib0  35970  dib1dim2  35974  diclspsn  36000  cdlemn8  36010  dihopelvalcpre  36054  djhcom  36211
  Copyright terms: Public domain W3C validator