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

Theorem 3eqtr4a 2493
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 2483 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2470 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  uniintsn  4079  iununi  4167  unizlim  4689  ordunisuc  4803  dmxpid  5080  rnxpid  5293  dmsnsnsn  5339  opswap  5347  xpcoid  5406  fvco4i  5792  fndmdifcom  5826  offres  6310  1stval2  6355  2ndval2  6356  cnvf1olem  6435  fparlem3  6439  fparlem4  6440  seqomlem1  6698  ecovcom  7006  ecovass  7007  ecovdi  7008  resixpfo  7091  mapunen  7267  cardidm  7835  cardiun  7858  alephcard  7940  cardalephex  7960  cardcf  8121  cfidm  8144  alephsing  8145  itunisuc  8288  itunitc  8290  ituniiun  8291  alephadd  8441  alephreg  8446  pwcfsdom  8447  addcompq  8816  addcomnq  8817  mulcompq  8818  mulcomnq  8819  addassnq  8824  mulassnq  8825  addid1  9235  zeo  10344  xnegneg  10789  xaddcom  10813  xaddid1  10814  xnegdi  10816  xmulid1  10847  xadddilem  10862  ixxin  10922  fzsuc2  11093  expneg  11377  sq01  11489  facp1  11559  bcpasc  11600  hashf1lem1  11692  hashf1  11694  eqs1  11749  absexp  12097  sqreulem  12151  fsumf1o  12505  fsumadd  12520  fsumrev2  12553  fsumparts  12573  fsumrelem  12574  efexp  12690  tanval2  12722  sqr2irrlem  12835  sadeq  12972  smumullem  12992  smumul  12993  gcdcom  13008  gcd0id  13011  gcdass  13033  nn0gcdsq  13132  dfphi2  13151  pcneg  13235  setscom  13485  strfvi  13495  setsnid  13497  ressbas  13507  ressinbas  13513  ressress  13514  firest  13648  topnval  13650  xpsfeq  13777  xpsaddlem  13788  xpsvsca  13792  homffval  13905  oppchomfval  13928  oppcbas  13932  rescbas  14017  rescco  14020  cofuass  14074  fucbas  14145  fuchom  14146  setccatid  14227  xpcbas  14263  xpchomfval  14264  xpccofval  14267  oduleval  14546  oduglb  14554  odulub  14556  ipotset  14571  grpinvfvi  14834  symgbas  15083  symggrp  15091  cntrval  15106  cntzval  15108  oppgplusfval  15132  sylow1lem2  15221  sylow3lem1  15249  oppglsm  15264  gsumzsplit  15517  gsum2d  15534  gsumcom2  15537  dprd2dlem2  15586  dprd2da  15588  dmdprdsplit2lem  15591  mgpplusg  15640  mgpress  15647  rngidval  15654  opprmulfval  15718  abvtrivd  15916  sralem  16237  srasca  16241  sravsca  16242  rlmval  16252  psrmulr  16436  mplmonmul  16515  mplcoe3  16517  opsrbaslem  16526  opsrtoslem2  16533  psr1val  16572  ply1basfvi  16623  ply1plusgfvi  16624  psr1sca2  16633  zlmlem  16786  zlmsca  16790  zlmvsca  16791  ocvval  16882  thlbas  16911  thlle  16912  thloc  16914  tgdif0  17045  indislem  17052  restco  17216  txtopon  17611  txindislem  17653  qtopres  17718  hmphindis  17817  ptuncnv  17827  snclseqg  18133  tsmssplit  18169  ussval  18277  tuslem  18285  setsmsbas  18493  tnglem  18669  tngds  18677  tngtset  18678  pcoass  19037  cphsqrcl2  19137  ovolunlem1a  19380  ioorinv  19456  itg11  19571  itg1mulc  19584  itg2cnlem1  19641  iblss2  19685  ibladdlem  19699  itgfsum  19706  iblabslem  19707  iblabs  19708  ditgneg  19732  deg1fvi  19996  dgrco  20181  logfac  20483  cxpexp  20547  cxpmul2  20568  cxpsqr  20582  dvcxp2  20615  ang180lem1  20639  mcubic  20675  quart1  20684  reasinsin  20724  atanlogaddlem  20741  atantayl2  20766  log2tlbnd  20773  basellem2  20852  basellem3  20853  basellem5  20855  basellem8  20858  dchrmulid2  21024  bcp1ctr  21051  lgsneg  21091  lgsneg1  21092  lgsdir2  21100  lgsdir  21102  lgsdi  21104  lgsquad2lem2  21131  pntleml  21293  eupath2lem3  21689  bafval  22071  ipidsq  22197  ipasslem1  22320  pjclem2  23687  cvmdi  23815  imadifxp  24026  iundisjcnt  24142  indval2  24400  sitgclcn  24646  sitgclre  24647  bayesth  24685  subfacp1lem6  24859  fprodf1o  25261  fprodmul  25273  fproddiv  25274  fprodfac  25285  fallfacfwd  25341  dfrdg2  25407  dfrdg3  25408  dfrdg4  25745  ordtoplem  26133  ordcmp  26145  mblfinlem  26190  itg2addnclem2  26203  ibladdnclem  26207  iblabsnclem  26214  iblabsnc  26215  iblmulc2nc  26216  kelac2  27078  dsmmval2  27117  m1expaddsub  27336  mendbas  27407  mendsca  27412  mendrng  27415  iotain  27532  addrcom  27594  itgsinexplem1  27662  swrdccatin1  28091  swrdccat3b  28106  dpfrac1  28373  pmodN  30486  tgrpgrplem  31385  tendoplass  31419  tendoicl  31432  erngdvlem3  31626  dvhvaddass  31734  dib0  31801  dib1dim2  31805  diclspsn  31831  cdlemn8  31841  dihopelvalcpre  31885  djhcom  32042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator