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

Theorem eqtr2d 2469
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1  |-  ( ph  ->  A  =  B )
eqtr2d.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eqtr2d  |-  ( ph  ->  C  =  A )

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 eqtr2d.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrd 2468 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2441 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  3eqtrrd  2473  3eqtr2rd  2475  ifan  3778  ifor  3779  dfopif  3981  onsucmin  4801  csbopeq1a  6400  oaabs2  6888  ecinxp  6979  resixpfo  7100  sbthlem3  7219  rankxpsuc  7806  fseqenlem2  7906  dfac2  8011  isf32lem9  8241  compsscnvlem  8250  ttukeylem7  8395  fpwwe2lem11  8515  00id  9241  submul2  9474  divadddiv  9729  infmsup  9986  xadd4d  10882  fzval3  11180  ceim1l  11234  fldiv  11241  flmod  11262  intfrac  11263  modcyc2  11277  moddi  11284  uzrdgfni  11298  axdc4uzlem  11321  seqf1olem1  11362  seqf1olem2  11363  seqid2  11369  expnegz  11414  binom2sub  11498  binom3  11500  ccatco  11804  swrds2  11880  reim  11914  mulre  11926  addcj  11953  absimle  12114  clim2ser  12448  isercoll2  12462  serf0  12474  iseralt  12478  summolem3  12508  isumclim3  12543  fsumrev  12562  fsumshft  12563  fsum2mul  12572  incexc  12617  isumsplit  12620  mertenslem1  12661  ef4p  12714  tanval3  12735  efival  12753  sinmul  12773  bitsinvp1  12961  sadaddlem  12978  bitsshft  12987  smu01lem  12997  eulerthlem2  13171  pythagtriplem16  13204  pczpre  13221  pcqdiv  13231  pcadd  13258  pcfac  13268  prmreclem5  13288  4sqlem10  13315  4sqlem19  13331  vdwapun  13342  vdwlem1  13349  ramcl  13397  strfvd  13498  strfv2d  13499  xpsff1o  13793  xpslem  13798  2oppccomf  13951  oppcepi  13965  sscfn1  14017  sscfn2  14018  invfuc  14171  grpinvval2  14872  pgp0  15230  sylow1lem1  15232  sylow3lem2  15262  efgredleme  15375  efgcpbllemb  15387  frgpuptinv  15403  frgpup3lem  15409  gexexlem  15467  cyggenod  15494  gsumval3eu  15513  gsumval3  15514  gsumzaddlem  15526  dprd2db  15601  rnginvdv  15799  lss1d  16039  mplcoe3  16529  subrgascl  16558  ply1sclid  16679  znzrh2  16826  ipassr2  16878  ntrval2  17115  ordtuni  17254  cnclima  17332  cmpsub  17463  ptbasfi  17613  txbasval  17638  pt1hmeo  17838  alexsubALTlem1  18078  trust  18259  ussid  18290  ressuss  18293  ressprdsds  18401  imasdsf1olem  18403  setsms  18510  tmsxms  18516  tmsxpsmopn  18567  subgnm  18674  tngnm  18692  tngngp2  18693  xrsxmet  18840  xrge0gsumle  18864  metdstri  18881  xrhmeo  18971  lebnumlem3  18988  pcorevlem  19051  pi1xfrcnvlem  19081  clmabs  19107  minveclem4a  19331  pjthlem1  19338  ovolunlem1a  19392  mbfres2  19537  i1faddlem  19585  ibladdlem  19711  iblabs  19720  ditgsplit  19748  dvnres  19817  dveflem  19863  dveq0  19884  dvfsumabs  19907  itgsubstlem  19932  evlseu  19937  ply1divex  20059  dgrco  20193  plycjlem  20194  taylthlem1  20289  pserdv2  20346  abelthlem6  20352  abelthlem7  20354  tangtx  20413  abssinper  20426  sineq0  20429  explog  20488  reexplog  20489  eflogeq  20496  abslogle  20513  tanarg  20514  logtayl  20551  logtayl2  20553  ang180lem3  20653  affineequiv  20667  affineequiv2  20668  chordthmlem4  20676  chordthmlem5  20677  dcubic1lem  20683  dcubic2  20684  dcubic  20686  mcubic  20687  cubic2  20688  dquartlem1  20691  dquart  20693  quart1lem  20695  quartlem1  20697  quart  20701  acoscos  20733  atanlogaddlem  20753  atantayl2  20778  atantayl3  20779  birthdaylem2  20791  efrlim  20808  amgmlem  20828  logdifbnd  20832  emcllem3  20836  emcllem6  20839  basellem3  20865  basellem8  20870  basellem9  20871  chtprm  20936  logfaclbnd  21006  perfect1  21012  bcp1ctr  21063  bclbnd  21064  bposlem1  21068  lgsdilem  21106  lgsdirnn0  21123  lgsdinn0  21124  lgseisenlem2  21134  lgsquadlem1  21138  2sqlem2  21148  mul2sq  21149  vmadivsum  21176  rpvmasumlem  21181  dchrisumlem1  21183  dchrisumlem2  21184  dchrmusum2  21188  dchrvmasum2if  21191  dchrisum0lem2  21212  logsqvma2  21237  selberg3  21253  selberg4lem1  21254  pntrsumo1  21259  pntrlog2bndlem2  21272  pntrlog2bndlem3  21273  pntrlog2bndlem5  21275  pntibndlem2  21285  pntlemk  21300  pntlemo  21301  ostth2lem4  21330  ostth3  21332  grpoidinvlem2  21793  gxid  21861  subgores  21892  nvmtri  22160  cnnvm  22174  nvnd  22180  ipidsq  22209  ipnm  22210  ipipcj  22214  blocnilem  22305  ipasslem2  22333  dipsubdir  22349  hvaddsubval  22535  pjhthlem1  22893  pjspansn  23079  pjo  23173  unoplin  23423  adjadj  23439  hmoplin  23445  eigvec1  23465  lnopeqi  23511  nmcexi  23529  lnfnsubi  23549  riesz3i  23565  kbass6  23624  leoprf2  23630  leoprf  23631  pjnmopi  23651  mdslmd1lem1  23828  mdslmd1lem2  23829  superpos  23857  xrge0tsmseq  24225  subrgchr  24230  rhmdvd  24259  pstmval  24290  mndpluscn  24312  qqhucn  24376  esumval  24441  gsumesum  24451  esumcst  24455  esumpcvgval  24468  probdif  24678  ballotlemfp1  24749  lgamgulmlem2  24814  lgamgulmlem3  24815  lgamgulmlem4  24816  lgamgulmlem5  24817  gamigam  24837  lgamcvg2  24839  gamfac  24851  derangen2  24860  subfaclefac  24862  subfaclim  24874  sinccvglem  25109  fprodshft  25300  fprodrev  25301  iprodclim3  25313  binomfallfaclem2  25356  brbtwn2  25844  colinearalglem4  25848  axsegconlem1  25856  axpaschlem  25879  axcontlem4  25906  axcontlem7  25909  axcontlem8  25910  ltflcei  26239  mblfinlem4  26246  ibladdnclem  26261  iblabsnc  26269  iblmulc2nc  26270  ftc1anclem6  26285  ftc1anclem8  26287  filnetlem4  26410  sdclem2  26446  ismtycnv  26511  heiborlem10  26529  mzpsubmpt  26800  irrapxlem3  26887  pellexlem6  26897  pell1234qrne0  26916  pell1234qrreccl  26917  pell1234qrmulcl  26918  pell14qrdich  26932  pell1qrgaplem  26936  rmxluc  26999  rmyluc  27000  jm2.24nn  27024  jm2.18  27059  jm2.19lem2  27061  jm2.19lem3  27062  jm2.22  27066  jm2.23  27067  jm2.16nn0  27075  jm2.27c  27078  fnwe2lem2  27126  lmhmfgsplit  27161  pwssplit1  27165  dsmmfi  27181  frlmlss  27196  frlmlbs  27226  frlmup3  27229  islindf4  27285  hbtlem2  27305  psgnunilem1  27393  psgnuni  27399  hashgcdeq  27494  dvconstbi  27528  stoweidlem22  27747  stoweidlem32  27757  wallispilem5  27794  stirlinglem5  27803  sigarcol  27830  swrdccatin12lem3  28212  swrdccatin12  28214  swrdccat3b  28219  2cshwmod  28257  cshweqrep  28274  frg2woteq  28449  recsec  28499  reccsc  28500  bnj1415  29407  lflvsass  29879  lkrscss  29896  eqlkr  29897  eqlkr3  29899  ldualvsdi2  29942  omllaw3  30043  cmtcomlemN  30046  cmtbr3N  30052  omlfh3N  30057  llnexchb2lem  30665  dalawlem7  30674  dalawlem11  30678  dalawlem12  30679  pol1N  30707  paddatclN  30746  4atexlemcnd  30869  ltrncoidN  30925  cdleme3b  31026  cdleme11  31067  cdleme15a  31071  cdleme22e  31141  cdleme22g  31145  cdlemg18b  31476  trlcoat  31520  cdlemk2  31629  cdlemk4  31631  cdlemki  31638  cdlemksv2  31644  cdlemk15  31652  cdlemk55a  31756  diainN  31855  dia2dimlem3  31864  dia2dimlem5  31866  dvhlveclem  31906  diaocN  31923  cdlemn4  31996  cdlemn8  32002  dihopelvalcpre  32046  dihmeetlem9N  32113  dih1dimatlem  32127  dihpN  32134  dochvalr3  32161  dochsat  32181  djhjlj  32201  dochdmm1  32208  dihjatcclem4  32219  dihjat1  32227  dihjat4  32231  dochsnkr2cl  32272  dochfl1  32274  lclkrlem2j  32314  mapdordlem2  32435  mapdrvallem2  32443  hdmap10  32641
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 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator