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

Theorem eqtr2d 2399
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 2398 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2371 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647
This theorem is referenced by:  3eqtrrd  2403  3eqtr2rd  2405  ifan  3693  ifor  3694  dfopif  3895  onsucmin  4715  csbopeq1a  6300  oaabs2  6785  ecinxp  6876  resixpfo  6997  sbthlem3  7116  rankxpsuc  7699  fseqenlem2  7799  dfac2  7904  isf32lem9  8134  compsscnvlem  8143  ttukeylem7  8289  fpwwe2lem11  8409  00id  9134  submul2  9367  divadddiv  9622  infmsup  9879  xadd4d  10775  fzval3  11068  ceim1l  11121  fldiv  11128  flmod  11149  intfrac  11150  modcyc2  11164  moddi  11171  uzrdgfni  11185  axdc4uzlem  11208  seqf1olem1  11249  seqf1olem2  11250  seqid2  11256  expnegz  11301  binom2sub  11385  binom3  11387  ccatco  11691  swrds2  11767  reim  11801  mulre  11813  addcj  11840  absimle  12001  clim2ser  12335  isercoll2  12349  serf0  12361  iseralt  12365  summolem3  12395  isumclim3  12430  fsumrev  12449  fsumshft  12450  fsum2mul  12459  incexc  12504  isumsplit  12507  mertenslem1  12548  ef4p  12601  tanval3  12622  efival  12640  sinmul  12660  bitsinvp1  12848  sadaddlem  12865  bitsshft  12874  smu01lem  12884  eulerthlem2  13058  pythagtriplem16  13091  pczpre  13108  pcqdiv  13118  pcadd  13145  pcfac  13155  prmreclem5  13175  4sqlem10  13202  4sqlem19  13218  vdwapun  13229  vdwlem1  13236  ramcl  13284  strfvd  13385  strfv2d  13386  xpsff1o  13680  xpslem  13685  2oppccomf  13838  oppcepi  13852  sscfn1  13904  sscfn2  13905  invfuc  14058  grpinvval2  14759  pgp0  15117  sylow1lem1  15119  sylow3lem2  15149  efgredleme  15262  efgcpbllemb  15274  frgpuptinv  15290  frgpup3lem  15296  gexexlem  15354  cyggenod  15381  gsumval3eu  15400  gsumval3  15401  gsumzaddlem  15413  dprd2db  15488  rnginvdv  15686  lss1d  15930  mplcoe3  16420  subrgascl  16449  ply1sclid  16573  znzrh2  16716  ipassr2  16768  ntrval2  17005  ordtuni  17137  cnclima  17214  cmpsub  17344  ptbasfi  17493  txbasval  17518  pt1hmeo  17714  alexsubALTlem1  17954  ressprdsds  18148  imasdsf1olem  18150  setsms  18239  tmsxms  18245  tmsxpsmopn  18296  subgnm  18362  tngnm  18380  tngngp2  18381  xrsxmet  18528  xrge0gsumle  18552  metdstri  18569  xrhmeo  18659  lebnumlem3  18676  pcorevlem  18739  pi1xfrcnvlem  18769  clmabs  18795  minveclem4a  19009  pjthlem1  19016  ovolunlem1a  19070  mbfres2  19215  i1faddlem  19263  ibladdlem  19389  iblabs  19398  ditgsplit  19426  dvnres  19495  dveflem  19541  dveq0  19562  dvfsumabs  19585  itgsubstlem  19610  evlseu  19615  ply1divex  19737  dgrco  19871  plycjlem  19872  taylthlem1  19967  pserdv2  20024  abelthlem6  20030  abelthlem7  20032  tangtx  20091  abssinper  20104  sineq0  20107  explog  20166  reexplog  20167  eflogeq  20174  abslogle  20191  tanarg  20192  logtayl  20229  logtayl2  20231  ang180lem3  20331  affineequiv  20345  affineequiv2  20346  chordthmlem4  20354  chordthmlem5  20355  dcubic1lem  20361  dcubic2  20362  dcubic  20364  mcubic  20365  cubic2  20366  dquartlem1  20369  dquart  20371  quart1lem  20373  quartlem1  20375  quart  20379  acoscos  20411  atanlogaddlem  20431  atantayl2  20456  atantayl3  20457  birthdaylem2  20469  efrlim  20486  amgmlem  20506  logdifbnd  20510  emcllem3  20514  emcllem6  20517  basellem3  20543  basellem8  20548  basellem9  20549  chtprm  20614  logfaclbnd  20684  perfect1  20690  bcp1ctr  20741  bclbnd  20742  bposlem1  20746  lgsdilem  20784  lgsdirnn0  20801  lgsdinn0  20802  lgseisenlem2  20812  lgsquadlem1  20816  2sqlem2  20826  mul2sq  20827  vmadivsum  20854  rpvmasumlem  20859  dchrisumlem1  20861  dchrisumlem2  20862  dchrmusum2  20866  dchrvmasum2if  20869  dchrisum0lem2  20890  logsqvma2  20915  selberg3  20931  selberg4lem1  20932  pntrsumo1  20937  pntrlog2bndlem2  20950  pntrlog2bndlem3  20951  pntrlog2bndlem5  20953  pntibndlem2  20963  pntlemk  20978  pntlemo  20979  ostth2lem4  21008  ostth3  21010  grpoidinvlem2  21183  gxid  21251  subgores  21282  nvmtri  21550  cnnvm  21564  nvnd  21570  ipidsq  21599  ipnm  21600  ipipcj  21604  blocnilem  21695  ipasslem2  21723  dipsubdir  21739  hvaddsubval  21925  pjhthlem1  22283  pjspansn  22469  pjo  22563  unoplin  22813  adjadj  22829  hmoplin  22835  eigvec1  22855  lnopeqi  22901  nmcexi  22919  lnfnsubi  22939  riesz3i  22955  kbass6  23014  leoprf2  23020  leoprf  23021  pjnmopi  23041  mdslmd1lem1  23218  mdslmd1lem2  23219  superpos  23247  xlt2addrd  23524  xrge0tsmseq  23616  rhmdvd  23624  mndpluscn  23667  trust  23732  ussid  23758  ressuss  23761  qqhval2lem  23837  gsumesum  23916  esumcst  23920  esumfzf  23924  esumpcvgval  23933  probdif  24126  ballotlemfp1  24197  lgamgulmlem2  24262  lgamgulmlem3  24263  lgamgulmlem4  24264  lgamgulmlem5  24265  gamigam  24285  lgamcvg2  24287  gamfac  24299  derangen2  24308  subfaclefac  24310  subfaclim  24322  sinccvglem  24592  fprodshft  24784  fprodrev  24785  iprodclim3  24790  brbtwn2  25275  colinearalglem4  25279  axsegconlem1  25287  axpaschlem  25310  axcontlem4  25337  axcontlem7  25340  axcontlem8  25341  ltflcei  25668  ibladdnclem  25679  iblabsnc  25687  iblmulc2nc  25688  filnetlem4  25837  sdclem2  25959  ismtycnv  26032  heiborlem10  26050  mzpsubmpt  26327  irrapxlem3  26415  pellexlem6  26425  pell1234qrne0  26444  pell1234qrreccl  26445  pell1234qrmulcl  26446  pell14qrdich  26460  pell1qrgaplem  26464  rmxluc  26527  rmyluc  26528  jm2.24nn  26552  jm2.18  26587  jm2.19lem2  26589  jm2.19lem3  26590  jm2.22  26594  jm2.23  26595  jm2.16nn0  26603  jm2.27c  26606  fnwe2lem2  26654  lmhmfgsplit  26690  pwssplit1  26694  dsmmfi  26710  frlmlss  26725  frlmlbs  26755  frlmup3  26758  islindf4  26814  hbtlem2  26834  psgnunilem1  26922  psgnuni  26928  hashgcdeq  27023  dvconstbi  27057  fmuldfeqlem1  27218  stoweidlem22  27277  stoweidlem32  27287  sigarcol  27360  recsec  27928  reccsc  27929  bnj1415  28832  lflvsass  29342  lkrscss  29359  eqlkr  29360  eqlkr3  29362  ldualvsdi2  29405  omllaw3  29506  cmtcomlemN  29509  cmtbr3N  29515  omlfh3N  29520  llnexchb2lem  30128  dalawlem7  30137  dalawlem11  30141  dalawlem12  30142  pol1N  30170  paddatclN  30209  4atexlemcnd  30332  ltrncoidN  30388  cdleme3b  30489  cdleme11  30530  cdleme15a  30534  cdleme22e  30604  cdleme22eALTN  30605  cdleme22g  30608  cdlemg18b  30939  trlcoat  30983  cdlemk2  31092  cdlemk4  31094  cdlemki  31101  cdlemksv2  31107  cdlemk15  31115  cdlemk55a  31219  diainN  31318  dia2dimlem3  31327  dia2dimlem5  31329  dvhlveclem  31369  diaocN  31386  cdlemn4  31459  cdlemn8  31465  dihopelvalcpre  31509  dihmeetlem9N  31576  dih1dimatlem  31590  dihpN  31597  dochvalr3  31624  dochsat  31644  djhjlj  31664  dochdmm1  31671  dihjatcclem4  31682  dihjat1  31690  dihjat4  31694  dochsnkr2cl  31735  dochfl1  31737  lclkrlem2j  31777  mapdordlem2  31898  mapdrvallem2  31906  hdmap10  32104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359
  Copyright terms: Public domain W3C validator