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

Theorem 3eqtr4a 2496
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 2486 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2473 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653
This theorem is referenced by:  uniintsn  4089  iinvdif  4165  iununi  4178  unizlim  4701  ordunisuc  4815  dmxpid  5092  rnxpid  5305  dmsnsnsn  5351  opswap  5359  xpcoid  5418  fvco4i  5804  fndmdifcom  5838  offres  6322  1stval2  6367  2ndval2  6368  cnvf1olem  6447  fparlem3  6451  fparlem4  6452  seqomlem1  6710  ecovcom  7018  ecovass  7019  ecovdi  7020  resixpfo  7103  mapunen  7279  cardidm  7851  cardiun  7874  alephcard  7956  cardalephex  7976  cardcf  8137  cfidm  8160  alephsing  8161  itunisuc  8304  itunitc  8306  ituniiun  8307  alephadd  8457  alephreg  8462  pwcfsdom  8463  addcompq  8832  addcomnq  8833  mulcompq  8834  mulcomnq  8835  addassnq  8840  mulassnq  8841  addid1  9251  zeo  10360  xnegneg  10805  xaddcom  10829  xaddid1  10830  xnegdi  10832  xmulid1  10863  xadddilem  10878  ixxin  10938  fzsuc2  11109  expneg  11394  sq01  11506  facp1  11576  bcpasc  11617  hashf1lem1  11709  hashf1  11711  eqs1  11766  absexp  12114  sqreulem  12168  fsumf1o  12522  fsumadd  12537  fsumrev2  12570  fsumparts  12590  fsumrelem  12591  efexp  12707  tanval2  12739  sqr2irrlem  12852  sadeq  12989  smumullem  13009  smumul  13010  gcdcom  13025  gcd0id  13028  gcdass  13050  nn0gcdsq  13149  dfphi2  13168  pcneg  13252  setscom  13502  strfvi  13512  setsnid  13514  ressbas  13524  ressinbas  13530  ressress  13531  firest  13665  topnval  13667  xpsfeq  13794  xpsaddlem  13805  xpsvsca  13809  homffval  13922  oppchomfval  13945  oppcbas  13949  rescbas  14034  rescco  14037  cofuass  14091  fucbas  14162  fuchom  14163  setccatid  14244  xpcbas  14280  xpchomfval  14281  xpccofval  14284  oduleval  14563  oduglb  14571  odulub  14573  ipotset  14588  grpinvfvi  14851  symgbas  15100  symggrp  15108  cntrval  15123  cntzval  15125  oppgplusfval  15149  sylow1lem2  15238  sylow3lem1  15266  oppglsm  15281  gsumzsplit  15534  gsum2d  15551  gsumcom2  15554  dprd2dlem2  15603  dprd2da  15605  dmdprdsplit2lem  15608  mgpplusg  15657  mgpress  15664  rngidval  15671  opprmulfval  15735  abvtrivd  15933  sralem  16254  srasca  16258  sravsca  16259  rlmval  16269  psrmulr  16453  mplmonmul  16532  mplcoe3  16534  opsrbaslem  16543  opsrtoslem2  16550  psr1val  16589  ply1basfvi  16640  ply1plusgfvi  16641  psr1sca2  16650  zlmlem  16803  zlmsca  16807  zlmvsca  16808  ocvval  16899  thlbas  16928  thlle  16929  thloc  16931  tgdif0  17062  indislem  17069  restco  17233  txtopon  17628  txindislem  17670  qtopres  17735  hmphindis  17834  ptuncnv  17844  snclseqg  18150  tsmssplit  18186  ussval  18294  tuslem  18302  setsmsbas  18510  tnglem  18686  tngds  18694  tngtset  18695  pcoass  19054  cphsqrcl2  19154  ovolunlem1a  19397  ioorinv  19473  itg11  19586  itg1mulc  19599  itg2cnlem1  19656  iblss2  19700  ibladdlem  19714  itgfsum  19721  iblabslem  19722  iblabs  19723  ditgneg  19749  deg1fvi  20013  dgrco  20198  logfac  20500  cxpexp  20564  cxpmul2  20585  cxpsqr  20599  dvcxp2  20632  ang180lem1  20656  mcubic  20692  quart1  20701  reasinsin  20741  atanlogaddlem  20758  atantayl2  20783  log2tlbnd  20790  basellem2  20869  basellem3  20870  basellem5  20872  basellem8  20875  dchrmulid2  21041  bcp1ctr  21068  lgsneg  21108  lgsneg1  21109  lgsdir2  21117  lgsdir  21119  lgsdi  21121  lgsquad2lem2  21148  pntleml  21310  eupath2lem3  21706  bafval  22088  ipidsq  22214  ipasslem1  22337  pjclem2  23704  cvmdi  23832  imadifxp  24043  iundisjcnt  24159  indval2  24417  sitgclcn  24663  sitgclre  24664  bayesth  24702  subfacp1lem6  24876  fprodf1o  25277  fprodmul  25289  fproddiv  25290  fprodfac  25301  fallfacfwd  25357  dfrdg2  25428  dfrdg3  25429  dfrdg4  25800  ordtoplem  26190  ordcmp  26202  mblfinlem2  26256  itg2addnclem2  26271  ibladdnclem  26275  iblabsnclem  26282  iblabsnc  26283  iblmulc2nc  26284  ftc1anclem8  26301  kelac2  27154  dsmmval2  27193  m1expaddsub  27412  mendbas  27483  mendsca  27488  mendrng  27491  iotain  27608  addrcom  27670  itgsinexplem1  27738  swrdccatin1  28239  swrdccat3blem  28252  dpfrac1  28589  pmodN  30721  tgrpgrplem  31620  tendoplass  31654  tendoicl  31667  erngdvlem3  31861  dvhvaddass  31969  dib0  32036  dib1dim2  32040  diclspsn  32066  cdlemn8  32076  dihopelvalcpre  32120  djhcom  32277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431
  Copyright terms: Public domain W3C validator