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

Theorem eqtr2d 2857
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1 (𝜑𝐴 = 𝐵)
eqtr2d.2 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
eqtr2d (𝜑𝐶 = 𝐴)

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 eqtr2d.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2856 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2827 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  3eqtrrd  2861  3eqtr2rd  2863  ifan  4516  ifor  4517  dfopif  4794  nvocnv  7029  elovmpt3rab1  7394  onsucmin  7524  csbopeq1a  7740  oaabs2  8262  ecinxp  8362  resixpfo  8489  sbthlem3  8618  rankxpsuc  9300  fseqenlem2  9440  dfac2b  9545  isf32lem9  9772  compsscnvlem  9781  ttukeylem7  9926  fpwwe2lem11  10051  00id  10804  submul2  11069  mulsubfacd  11090  divadddiv  11344  infrenegsup  11613  xadd4d  12686  fzdifsuc  12957  fzval3  13096  fzoshftral  13144  ceim1l  13205  fldiv  13218  flmod  13243  intfrac  13244  modcyc2  13265  moddi  13297  uzrdgfni  13316  axdc4uzlem  13341  seqf1olem1  13399  seqf1olem2  13400  seqid2  13406  expnegz  13453  binom2sub  13571  binom3  13575  hashreshashfun  13790  ccatw2s1p2  13987  ccats1pfxeq  14066  pfxccatin12lem2  14083  pfxccatin12  14085  swrdccat3b  14092  cshweqrep  14173  2cshwcshw  14177  ccatco  14187  swrds2  14292  relexpsucnnr  14374  relexpaddnn  14400  reim  14458  mulre  14470  addcj  14497  absimle  14659  clim2ser  15001  isercoll2  15015  serf0  15027  iseralt  15031  summolem3  15061  isumclim3  15104  mptfzshft  15123  fsumrev  15124  fsum2mul  15134  incexc  15182  isumsplit  15185  mertenslem1  15230  fprodrev  15321  iprodclim3  15344  binomfallfaclem2  15384  ef4p  15456  tanval3  15477  efival  15495  sinmul  15515  bitsinvp1  15788  sadaddlem  15805  bitsshft  15814  smu01lem  15824  dfgcd2  15884  lcmgcdlem  15940  lcm1  15944  lcmfass  15980  eulerthlem2  16109  hashgcdeq  16116  powm2modprm  16130  pythagtriplem16  16157  pczpre  16174  pcqdiv  16184  pcadd  16215  pcfac  16225  prmreclem5  16246  4sqlem10  16273  4sqlem19  16289  vdwapun  16300  vdwlem1  16307  ramcl  16355  setsstruct  16513  strfvd  16518  strfv2d  16519  xpsff1o  16830  xpsrnbas  16834  2oppccomf  16985  oppcepi  16999  sscfn1  17077  sscfn2  17078  invfuc  17234  funcestrcsetclem7  17386  funcsetcestrclem7  17401  gsumsplit1r  17887  grpinvssd  18116  grpinvval2  18122  cycsubggend  18288  pmtrdifwrdellem2  18541  psgnunilem1  18552  psgnuni  18558  pgp0  18652  sylow1lem1  18654  sylow3lem2  18684  efgredleme  18800  efgcpbllemb  18812  frgpuptinv  18828  frgpup3lem  18834  gexexlem  18903  cyggenod  18934  gsumval3eu  18955  gsumval3  18958  gsumzaddlem  18972  dprd2db  19096  ablsimpgfindlem1  19160  ringinvdv  19375  lss1d  19666  pwssplit1  19762  mplcoe3  20177  subrgascl  20208  evlseu  20226  mhpinvcl  20269  ply1sclid  20386  znzrh2  20622  regsumsupp  20696  ipassr2  20721  dsmmfi  20812  frlmlss  20825  frlmip  20852  frlmlbs  20871  frlmup3  20874  islindf4  20912  1marepvmarrepid  21114  madurid  21183  smadiadetlem3  21207  mat2pmatghm  21268  pmatcollpwscmatlem1  21327  pm2mpmhmlem2  21357  cpmadurid  21405  cpmidgsumm2pm  21407  cpmadugsumlemB  21412  cayhamlem2  21422  ntrval2  21589  ordtuni  21728  cnclima  21806  cmpsub  21938  ptbasfi  22119  txbasval  22144  pt1hmeo  22344  alexsubALTlem1  22585  trust  22767  ussid  22798  ressuss  22801  ressprdsds  22910  imasdsf1olem  22912  setsms  23019  tmsxms  23025  tmsxpsmopn  23076  subgnm  23171  tngnm  23189  tngngp2  23190  xrsxmet  23346  xrge0gsumle  23370  metdstri  23388  xrhmeo  23479  lebnumlem3  23496  pcorevlem  23559  pi1xfrcnvlem  23589  clmabs  23616  cvsmuleqdivd  23667  rrxip  23922  rrxds  23925  rrxdsfi  23943  minveclem4a  23962  pjthlem1  23969  divcncf  23977  ovolunlem1a  24026  mbfres2  24175  i1faddlem  24223  ibladdlem  24349  iblabs  24358  ditgsplit  24388  dvnres  24457  dvmptdiv  24500  dveflem  24505  dveq0  24526  dvfsumabs  24549  itgsubstlem  24574  ply1divex  24659  dgrco  24794  plycjlem  24795  taylthlem1  24890  pserdv2  24947  abelthlem6  24953  abelthlem7  24955  tangtx  25020  abssinper  25035  sineq0  25038  explog  25104  reexplog  25105  eflogeq  25112  abslogle  25128  tanarg  25129  logtayl  25170  logtayl2  25172  relogbdiv  25284  ang180lem3  25316  affineequiv  25328  affineequiv2  25329  chordthmlem4  25340  chordthmlem5  25341  heron  25343  dcubic1lem  25348  dcubic2  25349  dcubic  25351  mcubic  25352  cubic2  25353  dquartlem1  25356  dquart  25358  quart1lem  25360  quartlem1  25362  quart  25366  acoscos  25398  atanlogaddlem  25418  atantayl2  25443  atantayl3  25444  birthdaylem2  25458  efrlim  25475  amgmlem  25495  logdifbnd  25499  emcllem3  25503  emcllem6  25506  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  gamigam  25558  lgamcvg2  25560  gamfac  25572  basellem3  25588  basellem8  25593  basellem9  25594  chtprm  25658  logfaclbnd  25726  perfect1  25732  bcp1ctr  25783  bclbnd  25784  bposlem1  25788  lgsdilem  25828  lgsdirnn0  25848  lgsdinn0  25849  gausslemma2dlem1a  25869  gausslemma2dlem4  25873  gausslemma2dlem5a  25874  lgseisenlem2  25880  lgsquadlem1  25884  2sqlem2  25922  mul2sq  25923  2sqmod  25940  2sqnn0  25942  vmadivsum  25986  rpvmasumlem  25991  dchrisumlem1  25993  dchrisumlem2  25994  dchrmusum2  25998  dchrvmasum2if  26001  dchrisum0lem2  26022  logsqvma2  26047  selberg3  26063  selberg4lem1  26064  pntrsumo1  26069  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem5  26085  pntibndlem2  26095  pntlemk  26110  pntlemo  26111  ostth2lem4  26140  ostth3  26142  tgbtwndiff  26220  tgifscgr  26222  trgcgrg  26229  motcgr3  26259  tgbtwnconn1lem1  26286  tgbtwnconn1lem2  26287  ismir  26373  miriso  26384  midexlem  26406  ragmir  26414  footexALT  26432  footexlem1  26433  footexlem2  26434  colperpexlem3  26446  mideulem2  26448  midex  26451  opphllem3  26463  midcgr  26494  lmiisolem  26510  brbtwn2  26619  colinearalglem4  26623  axsegconlem1  26631  axpaschlem  26654  axcontlem4  26681  axcontlem7  26684  axcontlem8  26685  ushgredgedgloop  26941  crctcshwlkn0lem6  27521  wwlknlsw  27553  wwlksnextwrd  27603  clwlkclwwlklem2a3  27700  clwlkclwwlk2  27709  clwwlkel  27753  clwwlkfo  27757  clwwlkext2edg  27763  eupth2eucrct  27924  numclwwlk2lem1lem  28049  numclwwlk1lem2fo  28065  numclwlk2lem2f  28084  grpoidinvlem2  28210  nvmtri  28376  cnnvm  28387  nvnd  28393  ipidsq  28415  ipnm  28416  ipipcj  28420  blocnilem  28509  ipasslem2  28537  dipsubdir  28553  hvaddsubval  28738  pjhthlem1  29096  pjspansn  29282  pjo  29376  unoplin  29625  adjadj  29641  hmoplin  29647  eigvec1  29667  lnopeqi  29713  nmcexi  29731  lnfnsubi  29751  riesz3i  29767  kbass6  29826  leoprf2  29832  leoprf  29833  pjnmopi  29853  mdslmd1lem1  30030  mdslmd1lem2  30031  superpos  30059  ifeq3da  30229  fgreu  30346  resf1o  30393  fprodex01  30469  wrdt2ind  30555  gsummpt2d  30615  xrge0tsmseq  30622  symgfcoeu  30654  psgnfzto1stlem  30670  psgnfzto1st  30675  cycpm2tr  30689  cycpmco2lem6  30701  cycpmco2lem7  30702  subrgchr  30793  rhmdvd  30822  dimval  30901  dimvalfi  30902  lindsunlem  30920  dimkerim  30923  qusdimsum  30924  fedgmullem1  30925  fedgmullem2  30926  extdg1id  30953  madjusmdetlem2  30993  qtophaus  31000  pstmval  31035  mndpluscn  31069  qqhucn  31133  esumval  31205  gsumesum  31218  esumcst  31222  esumpcvgval  31237  oddpwdc  31512  eulerpartlemgvv  31534  probdif  31578  sgnmul  31700  signsvtn  31754  actfunsnf1o  31775  reprpmtf1o  31797  hgt750lemd  31819  logdivsqrle  31821  hgt750lemg  31825  hgt750lemb  31827  bnj1415  32208  swrdrevpfx  32261  pfxwlk  32268  derangen2  32319  subfaclefac  32321  subfaclim  32333  satom  32501  fmla  32526  mrsubrn  32658  sinccvglem  32813  bcprod  32868  filnetlem4  33627  curunc  34756  ltflcei  34762  matunitlindflem1  34770  matunitlindflem2  34771  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem24  34798  mblfinlem4  34814  ibladdnclem  34830  iblabsnc  34838  iblmulc2nc  34839  ftc1anclem6  34854  ftc1anclem8  34856  sdclem2  34900  ismtycnv  34963  heiborlem10  34981  lflvsass  36099  lkrscss  36116  eqlkr  36117  eqlkr3  36119  ldualvsdi2  36162  omllaw3  36263  cmtcomlemN  36266  cmtbr3N  36272  omlfh3N  36277  llnexchb2lem  36886  dalawlem7  36895  dalawlem11  36899  dalawlem12  36900  pol1N  36928  paddatclN  36967  4atexlemcnd  37090  ltrncoidN  37146  cdleme3b  37247  cdleme11  37288  cdleme15a  37292  cdleme22e  37362  cdleme22g  37366  cdlemg18b  37697  trlcoat  37741  cdlemk2  37850  cdlemk4  37852  cdlemki  37859  cdlemksv2  37865  cdlemk15  37873  cdlemk55a  37977  diainN  38075  dia2dimlem3  38084  dia2dimlem5  38086  dvhlveclem  38126  diaocN  38143  cdlemn4  38216  cdlemn8  38222  dihopelvalcpre  38266  dihmeetlem9N  38333  dih1dimatlem  38347  dihpN  38354  dochvalr3  38381  dochsat  38401  djhjlj  38421  dochdmm1  38428  dihjatcclem4  38439  dihjat1  38447  dihjat4  38451  dochsnkr2cl  38492  dochfl1  38494  lclkrlem2j  38534  mapdordlem2  38655  mapdrvallem2  38663  hdmap10  38858  frlmvscadiccat  39025  frlmsnic  39029  negexpidd  39159  3cubeslem2  39162  3cubeslem3r  39164  mzpsubmpt  39220  irrapxlem3  39301  pellexlem6  39311  pell1234qrne0  39330  pell1234qrreccl  39331  pell1234qrmulcl  39332  pell14qrdich  39346  pell1qrgaplem  39350  rmxluc  39413  rmyluc  39414  jm2.24nn  39436  jm2.18  39465  jm2.19lem2  39467  jm2.19lem3  39468  jm2.22  39472  jm2.23  39473  jm2.16nn0  39481  jm2.27c  39484  fnwe2lem2  39531  lmhmfgsplit  39566  hbtlem2  39604  relexpmulnn  39934  relexpmulg  39935  ntrclsneine0lem  40294  int-addassocd  40408  dvconstbi  40546  bccm1k  40554  binomcxplemnotnn0  40568  fmptsnxp  41305  wessf1ornlem  41325  disjinfi  41334  projf1o  41339  infnsuprnmpt  41402  lefldiveq  41439  lt4addmuld  41453  fzdifsuc2  41457  suplesup  41487  infrpge  41499  xrlexaddrp  41500  xralrple2  41502  infleinflem1  41518  supminfrnmpt  41599  supminfxr2  41625  fsumnncl  41732  limcperiod  41789  sumnnodd  41791  limcresiooub  41803  limcresioolb  41804  0ellimcdiv  41810  reclimc  41814  limsupval3  41853  limsupequzmpt2  41879  liminfval5  41926  limsupresxr  41927  liminfresxr  41928  liminfvalxr  41944  liminfequzmpt2  41952  climliminflimsupd  41962  liminfltlem  41965  liminflbuz2  41976  sinmulcos  42026  coskpi2  42027  cncfdmsn  42053  cncfiooicclem1  42056  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  fperdvper  42083  dvmptresicc  42084  dvnmptdivc  42103  dvnxpaek  42107  dvnmul  42108  dvnprodlem1  42111  dvnprodlem3  42113  itgcoscmulx  42134  itgsincmulx  42139  itgspltprt  42144  itgiccshift  42145  itgperiod  42146  sublevolico  42150  volioof  42153  ovolsplit  42154  fvvolioof  42155  fvvolicof  42157  stoweidlem22  42188  stoweidlem32  42198  wallispilem5  42235  stirlinglem5  42244  dirkertrigeqlem2  42265  dirkertrigeq  42267  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem13  42286  fourierdlem16  42289  fourierdlem19  42292  fourierdlem21  42294  fourierdlem22  42295  fourierdlem28  42301  fourierdlem32  42305  fourierdlem33  42306  fourierdlem42  42315  fourierdlem47  42319  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem56  42328  fourierdlem60  42332  fourierdlem61  42333  fourierdlem64  42336  fourierdlem66  42338  fourierdlem71  42343  fourierdlem73  42345  fourierdlem74  42346  fourierdlem76  42348  fourierdlem78  42350  fourierdlem79  42351  fourierdlem80  42352  fourierdlem81  42353  fourierdlem83  42355  fourierdlem88  42360  fourierdlem92  42364  fourierdlem93  42365  fourierdlem97  42369  fourierdlem101  42373  fourierdlem103  42375  fourierdlem104  42376  fourierdlem109  42381  fourierdlem111  42383  fouriersw  42397  elaa2lem  42399  etransclem24  42424  etransclem25  42425  etransclem35  42435  etransclem46  42446  rrndistlt  42456  rrxunitopnfi  42458  qndenserrnbl  42461  qndenserrnopnlem  42463  saldifcl2  42492  intsal  42494  sge0sn  42542  sge0ltfirp  42563  sge0iunmptlemre  42578  sge0fodjrnlem  42579  sge0isum  42590  sge0xaddlem1  42596  nnfoctbdjlem  42618  meassle  42626  ismeannd  42630  meadif  42642  meaiuninclem  42643  meaiininclem  42649  omeunile  42668  caragendifcl  42677  caratheodory  42691  isomenndlem  42693  ovnsubaddlem1  42733  hoidmv1lelem2  42755  hoidmv1le  42757  hoidmvlelem2  42759  hoidmvle  42763  hoi2toco  42770  rrnmbl  42777  hoidifhspdmvle  42783  voncmpl  42784  hoiqssbl  42788  hspmbllem1  42789  hspmbllem2  42790  ovolval2lem  42806  ovolval5lem2  42816  ovnovollem1  42819  ovnovollem2  42820  hoimbl2  42828  vonhoire  42835  salpreimagelt  42867  salpreimalegt  42869  preimaioomnf  42878  smfres  42946  smfmullem1  42947  smflimmpt  42965  smfsupmpt  42970  smfinfmpt  42974  smflimsupmpt  42984  smfliminflem  42985  smfliminfmpt  42987  sigarcol  43002  f1oresf1o  43370  elsprel  43484  prproropf1o  43516  paireqne  43520  sfprmdvdsmersenne  43615  lighneallem3  43619  lighneallem4  43622  nn0onn0exALTV  43711  nnsum3primesprm  43802  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  c0snmgmhm  44083  rngcifuestrc  44166  funcrngcsetc  44167  funcrngcsetcALT  44168  funcringcsetc  44204  funcringcsetcALTV2lem7  44211  funcringcsetclem7ALTV  44234  lincext3  44409  lincresunit3  44434  nn0onn0ex  44481  nnpw2pmod  44541  blennn0em1  44549  digexp  44565  dignn0ehalf  44575  nn0mulfsum  44582  eenglngeehlnmlem2  44623  rrx2vlinest  44626  line2  44637  itschlc0xyqsol  44652  itsclinecirc0b  44659  recsec  44753  reccsc  44754  aacllem  44800  amgmlemALT  44802
  Copyright terms: Public domain W3C validator