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

Theorem eqtr2d 2329
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 2328 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2301 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  3eqtrrd  2333  3eqtr2rd  2335  ifan  3617  ifor  3618  dfopif  3809  onsucmin  4628  csbopeq1a  6189  oaabs2  6659  ecinxp  6750  resixpfo  6870  sbthlem3  6989  rankxpsuc  7568  fseqenlem2  7668  dfac2  7773  isf32lem9  8003  compsscnvlem  8012  ttukeylem7  8158  fpwwe2lem11  8278  00id  9003  submul2  9236  divadddiv  9491  infmsup  9748  fzval3  10927  ceim1l  10973  fldiv  10980  flmod  11001  intfrac  11002  modcyc2  11016  moddi  11023  uzrdgfni  11037  axdc4uzlem  11060  seqf1olem1  11101  seqf1olem2  11102  seqid2  11108  expnegz  11152  binom2sub  11236  binom3  11238  ccatco  11506  swrds2  11576  reim  11610  mulre  11622  addcj  11649  absimle  11810  clim2ser  12144  isercoll2  12158  serf0  12169  iseralt  12173  summolem3  12203  isumclim3  12238  fsumrev  12257  fsumshft  12258  fsum2mul  12267  incexc  12312  isumsplit  12315  mertenslem1  12356  ef4p  12409  tanval3  12430  efival  12448  sinmul  12468  bitsinvp1  12656  sadaddlem  12673  bitsshft  12682  smu01lem  12692  eulerthlem2  12866  pythagtriplem16  12899  pczpre  12916  pcqdiv  12926  pcadd  12953  pcfac  12963  prmreclem5  12983  4sqlem10  13010  4sqlem19  13026  vdwapun  13037  vdwlem1  13044  ramcl  13092  strfvd  13193  strfv2d  13194  xpsff1o  13486  xpslem  13491  2oppccomf  13644  oppcepi  13658  sscfn1  13710  sscfn2  13711  invfuc  13864  grpinvval2  14565  pgp0  14923  sylow1lem1  14925  sylow3lem2  14955  efgredleme  15068  efgcpbllemb  15080  frgpuptinv  15096  frgpup3lem  15102  gexexlem  15160  cyggenod  15187  gsumval3eu  15206  gsumval3  15207  gsumzaddlem  15219  dprd2db  15294  rnginvdv  15492  lss1d  15736  mplcoe3  16226  subrgascl  16255  ply1sclid  16379  znzrh2  16515  ipassr2  16567  ntrval2  16804  ordtuni  16936  cnclima  17013  cmpsub  17143  ptbasfi  17292  txbasval  17317  pt1hmeo  17513  alexsubALTlem1  17757  ressprdsds  17951  imasdsf1olem  17953  setsms  18042  tmsxms  18048  tmsxpsmopn  18099  subgnm  18165  tngnm  18183  tngngp2  18184  xrsxmet  18331  xrge0gsumle  18354  metdstri  18371  xrhmeo  18460  lebnumlem3  18477  pcorevlem  18540  pi1xfrcnvlem  18570  clmabs  18596  minveclem4a  18810  pjthlem1  18817  ovolunlem1a  18871  mbfres2  19016  i1faddlem  19064  ibladdlem  19190  iblabs  19199  ditgsplit  19227  dvnres  19296  dveflem  19342  dveq0  19363  dvfsumabs  19386  itgsubstlem  19411  evlseu  19416  ply1divex  19538  dgrco  19672  plycjlem  19673  taylthlem1  19768  pserdv2  19822  abelthlem6  19828  abelthlem7  19830  tangtx  19889  abssinper  19902  sineq0  19905  explog  19963  reexplog  19964  eflogeq  19971  tanarg  19986  logtayl  20023  logtayl2  20025  ang180lem3  20125  affineequiv  20139  affineequiv2  20140  chordthmlem4  20148  chordthmlem5  20149  dcubic1lem  20155  dcubic2  20156  dcubic  20158  mcubic  20159  cubic2  20160  dquartlem1  20163  dquart  20165  quart1lem  20167  quartlem1  20169  quart  20173  acoscos  20205  atanlogaddlem  20225  atantayl2  20250  atantayl3  20251  birthdaylem2  20263  efrlim  20280  amgmlem  20300  logdifbnd  20304  emcllem3  20307  emcllem6  20310  basellem3  20336  basellem8  20341  basellem9  20342  chtprm  20407  logfaclbnd  20477  perfect1  20483  bcp1ctr  20534  bclbnd  20535  bposlem1  20539  lgsdilem  20577  lgsdirnn0  20594  lgsdinn0  20595  lgseisenlem2  20605  lgsquadlem1  20609  2sqlem2  20619  mul2sq  20620  vmadivsum  20647  rpvmasumlem  20652  dchrisumlem1  20654  dchrisumlem2  20655  dchrmusum2  20659  dchrvmasum2if  20662  dchrisum0lem2  20683  logsqvma2  20708  selberg3  20724  selberg4lem1  20725  pntrsumo1  20730  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntibndlem2  20756  pntlemk  20771  pntlemo  20772  ostth2lem4  20801  ostth3  20803  grpoidinvlem2  20888  gxid  20956  subgores  20987  nvmtri  21253  cnnvm  21267  nvnd  21273  ipidsq  21302  ipnm  21303  ipipcj  21307  blocnilem  21398  ipasslem2  21426  dipsubdir  21442  hvaddsubval  21628  pjhthlem1  21986  pjspansn  22172  pjo  22266  unoplin  22516  adjadj  22532  hmoplin  22538  eigvec1  22558  lnopeqi  22604  nmcexi  22622  lnfnsubi  22642  riesz3i  22658  kbass6  22717  leoprf2  22723  leoprf  22724  pjnmopi  22744  mdslmd1lem1  22921  mdslmd1lem2  22922  superpos  22950  ballotlemfp1  23066  xlt2addrd  23268  mndpluscn  23314  xrge0tsmseq  23399  esumcst  23451  esumpcvgval  23461  probdif  23638  derangen2  23720  subfaclefac  23722  subfaclim  23734  sinccvglem  24020  brbtwn2  24605  colinearalglem4  24609  axsegconlem1  24617  axpaschlem  24640  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  ltflcei  24998  ibladdnclem  25007  iblabsnc  25015  iblmulc2nc  25016  svs3  25591  2wsms  25711  lvsovso  25729  idsubfun  25961  morexcmp  26070  lineval42  26183  filnetlem4  26433  sdclem2  26555  ismtycnv  26629  heiborlem10  26647  mzpsubmpt  26924  irrapxlem3  27012  pellexlem6  27022  pell1234qrne0  27041  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell14qrdich  27057  pell1qrgaplem  27061  rmxluc  27124  rmyluc  27125  jm2.24nn  27149  jm2.18  27184  jm2.19lem2  27186  jm2.19lem3  27187  jm2.22  27191  jm2.23  27192  jm2.16nn0  27200  jm2.27c  27203  fnwe2lem2  27251  lmhmfgsplit  27287  pwssplit1  27291  dsmmfi  27307  frlmlss  27322  frlmlbs  27352  frlmup3  27355  islindf4  27411  hbtlem2  27431  psgnunilem1  27519  psgnuni  27525  hashgcdeq  27620  dvconstbi  27654  fmuldfeqlem1  27815  stoweidlem22  27874  stoweidlem32  27884  sigarcol  27957  recsec  28480  reccsc  28481  bnj1415  29384  lflvsass  29893  lkrscss  29910  eqlkr  29911  eqlkr3  29913  ldualvsdi2  29956  omllaw3  30057  cmtcomlemN  30060  cmtbr3N  30066  omlfh3N  30071  llnexchb2lem  30679  dalawlem7  30688  dalawlem11  30692  dalawlem12  30693  pol1N  30721  paddatclN  30760  4atexlemcnd  30883  ltrncoidN  30939  cdleme3b  31040  cdleme11  31081  cdleme15a  31085  cdleme22e  31155  cdleme22eALTN  31156  cdleme22g  31159  cdlemg18b  31490  trlcoat  31534  cdlemk2  31643  cdlemk4  31645  cdlemki  31652  cdlemksv2  31658  cdlemk15  31666  cdlemk55a  31770  diainN  31869  dia2dimlem3  31878  dia2dimlem5  31880  dvhlveclem  31920  diaocN  31937  cdlemn4  32010  cdlemn8  32016  dihopelvalcpre  32060  dihmeetlem9N  32127  dih1dimatlem  32141  dihpN  32148  dochvalr3  32175  dochsat  32195  djhjlj  32215  dochdmm1  32222  dihjatcclem4  32233  dihjat1  32241  dihjat4  32245  dochsnkr2cl  32286  dochfl1  32288  lclkrlem2j  32328  mapdordlem2  32449  mapdrvallem2  32457  hdmap10  32655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator