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

Theorem eqtr2d 2316
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 2315 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2288 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  3eqtrrd  2320  3eqtr2rd  2322  ifan  3604  ifor  3605  dfopif  3793  onsucmin  4612  csbopeq1a  6173  oaabs2  6643  ecinxp  6734  resixpfo  6854  sbthlem3  6973  rankxpsuc  7552  fseqenlem2  7652  dfac2  7757  isf32lem9  7987  compsscnvlem  7996  ttukeylem7  8142  fpwwe2lem11  8262  00id  8987  submul2  9220  divadddiv  9475  infmsup  9732  fzval3  10911  ceim1l  10957  fldiv  10964  flmod  10985  intfrac  10986  modcyc2  11000  moddi  11007  uzrdgfni  11021  axdc4uzlem  11044  seqf1olem1  11085  seqf1olem2  11086  seqid2  11092  expnegz  11136  binom2sub  11220  binom3  11222  ccatco  11490  swrds2  11560  reim  11594  mulre  11606  addcj  11633  absimle  11794  clim2ser  12128  isercoll2  12142  serf0  12153  iseralt  12157  summolem3  12187  isumclim3  12222  fsumrev  12241  fsumshft  12242  fsum2mul  12251  incexc  12296  isumsplit  12299  mertenslem1  12340  ef4p  12393  tanval3  12414  efival  12432  sinmul  12452  bitsinvp1  12640  sadaddlem  12657  bitsshft  12666  smu01lem  12676  eulerthlem2  12850  pythagtriplem16  12883  pczpre  12900  pcqdiv  12910  pcadd  12937  pcfac  12947  prmreclem5  12967  4sqlem10  12994  4sqlem19  13010  vdwapun  13021  vdwlem1  13028  ramcl  13076  strfvd  13177  strfv2d  13178  xpsff1o  13470  xpslem  13475  2oppccomf  13628  oppcepi  13642  sscfn1  13694  sscfn2  13695  invfuc  13848  grpinvval2  14549  pgp0  14907  sylow1lem1  14909  sylow3lem2  14939  efgredleme  15052  efgcpbllemb  15064  frgpuptinv  15080  frgpup3lem  15086  gexexlem  15144  cyggenod  15171  gsumval3eu  15190  gsumval3  15191  gsumzaddlem  15203  dprd2db  15278  rnginvdv  15476  lss1d  15720  mplcoe3  16210  subrgascl  16239  ply1sclid  16363  znzrh2  16499  ipassr2  16551  ntrval2  16788  ordtuni  16920  cnclima  16997  cmpsub  17127  ptbasfi  17276  txbasval  17301  pt1hmeo  17497  alexsubALTlem1  17741  ressprdsds  17935  imasdsf1olem  17937  setsms  18026  tmsxms  18032  tmsxpsmopn  18083  subgnm  18149  tngnm  18167  tngngp2  18168  xrsxmet  18315  xrge0gsumle  18338  metdstri  18355  xrhmeo  18444  lebnumlem3  18461  pcorevlem  18524  pi1xfrcnvlem  18554  clmabs  18580  minveclem4a  18794  pjthlem1  18801  ovolunlem1a  18855  mbfres2  19000  i1faddlem  19048  ibladdlem  19174  iblabs  19183  ditgsplit  19211  dvnres  19280  dveflem  19326  dveq0  19347  dvfsumabs  19370  itgsubstlem  19395  evlseu  19400  ply1divex  19522  dgrco  19656  plycjlem  19657  taylthlem1  19752  pserdv2  19806  abelthlem6  19812  abelthlem7  19814  tangtx  19873  abssinper  19886  sineq0  19889  explog  19947  reexplog  19948  eflogeq  19955  tanarg  19970  logtayl  20007  logtayl2  20009  ang180lem3  20109  affineequiv  20123  affineequiv2  20124  chordthmlem4  20132  chordthmlem5  20133  dcubic1lem  20139  dcubic2  20140  dcubic  20142  mcubic  20143  cubic2  20144  dquartlem1  20147  dquart  20149  quart1lem  20151  quartlem1  20153  quart  20157  acoscos  20189  atanlogaddlem  20209  atantayl2  20234  atantayl3  20235  birthdaylem2  20247  efrlim  20264  amgmlem  20284  logdifbnd  20288  emcllem3  20291  emcllem6  20294  basellem3  20320  basellem8  20325  basellem9  20326  chtprm  20391  logfaclbnd  20461  perfect1  20467  bcp1ctr  20518  bclbnd  20519  bposlem1  20523  lgsdilem  20561  lgsdirnn0  20578  lgsdinn0  20579  lgseisenlem2  20589  lgsquadlem1  20593  2sqlem2  20603  mul2sq  20604  vmadivsum  20631  rpvmasumlem  20636  dchrisumlem1  20638  dchrisumlem2  20639  dchrmusum2  20643  dchrvmasum2if  20646  dchrisum0lem2  20667  logsqvma2  20692  selberg3  20708  selberg4lem1  20709  pntrsumo1  20714  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntibndlem2  20740  pntlemk  20755  pntlemo  20756  ostth2lem4  20785  ostth3  20787  grpoidinvlem2  20872  gxid  20940  subgores  20971  nvmtri  21237  cnnvm  21251  nvnd  21257  ipidsq  21286  ipnm  21287  ipipcj  21291  blocnilem  21382  ipasslem2  21410  dipsubdir  21426  hvaddsubval  21612  pjhthlem1  21970  pjspansn  22156  pjo  22250  unoplin  22500  adjadj  22516  hmoplin  22522  eigvec1  22542  lnopeqi  22588  nmcexi  22606  lnfnsubi  22626  riesz3i  22642  kbass6  22701  leoprf2  22707  leoprf  22708  pjnmopi  22728  mdslmd1lem1  22905  mdslmd1lem2  22906  superpos  22934  ballotlemfp1  23050  xlt2addrd  23253  mndpluscn  23299  xrge0tsmseq  23384  esumcst  23436  esumpcvgval  23446  probdif  23623  derangen2  23705  subfaclefac  23707  subfaclim  23719  sinccvglem  24005  brbtwn2  24533  colinearalglem4  24537  axsegconlem1  24545  axpaschlem  24568  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  svs3  25488  2wsms  25608  lvsovso  25626  idsubfun  25858  morexcmp  25967  lineval42  26080  filnetlem4  26330  sdclem2  26452  ismtycnv  26526  heiborlem10  26544  mzpsubmpt  26821  irrapxlem3  26909  pellexlem6  26919  pell1234qrne0  26938  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrdich  26954  pell1qrgaplem  26958  rmxluc  27021  rmyluc  27022  jm2.24nn  27046  jm2.18  27081  jm2.19lem2  27083  jm2.19lem3  27084  jm2.22  27088  jm2.23  27089  jm2.16nn0  27097  jm2.27c  27100  fnwe2lem2  27148  lmhmfgsplit  27184  pwssplit1  27188  dsmmfi  27204  frlmlss  27219  frlmlbs  27249  frlmup3  27252  islindf4  27308  hbtlem2  27328  psgnunilem1  27416  psgnuni  27422  hashgcdeq  27517  dvconstbi  27551  fmuldfeqlem1  27712  stoweidlem22  27771  stoweidlem32  27781  sigarcol  27854  recsec  28226  reccsc  28227  bnj1415  29068  lflvsass  29271  lkrscss  29288  eqlkr  29289  eqlkr3  29291  ldualvsdi2  29334  omllaw3  29435  cmtcomlemN  29438  cmtbr3N  29444  omlfh3N  29449  llnexchb2lem  30057  dalawlem7  30066  dalawlem11  30070  dalawlem12  30071  pol1N  30099  paddatclN  30138  4atexlemcnd  30261  ltrncoidN  30317  cdleme3b  30418  cdleme11  30459  cdleme15a  30463  cdleme22e  30533  cdleme22eALTN  30534  cdleme22g  30537  cdlemg18b  30868  trlcoat  30912  cdlemk2  31021  cdlemk4  31023  cdlemki  31030  cdlemksv2  31036  cdlemk15  31044  cdlemk55a  31148  diainN  31247  dia2dimlem3  31256  dia2dimlem5  31258  dvhlveclem  31298  diaocN  31315  cdlemn4  31388  cdlemn8  31394  dihopelvalcpre  31438  dihmeetlem9N  31505  dih1dimatlem  31519  dihpN  31526  dochvalr3  31553  dochsat  31573  djhjlj  31593  dochdmm1  31600  dihjatcclem4  31611  dihjat1  31619  dihjat4  31623  dochsnkr2cl  31664  dochfl1  31666  lclkrlem2j  31706  mapdordlem2  31827  mapdrvallem2  31835  hdmap10  32033
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator