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

Theorem eqtr2d 2686
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 2685 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2657 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  3eqtrrd  2690  3eqtr2rd  2692  ifan  4167  ifor  4168  dfopif  4430  nvocnv  6577  elovmpt3rab1  6935  onsucmin  7063  csbopeq1a  7265  oaabs2  7770  ecinxp  7865  resixpfo  7988  sbthlem3  8113  rankxpsuc  8783  fseqenlem2  8886  dfac2  8991  isf32lem9  9221  compsscnvlem  9230  ttukeylem7  9375  fpwwe2lem11  9500  00id  10249  submul2  10508  mulsubfacd  10530  divadddiv  10778  infrenegsup  11044  xadd4d  12171  fzdifsuc  12438  fzval3  12576  fzoshftral  12625  ceim1l  12686  fldiv  12699  flmod  12724  intfrac  12725  modcyc2  12746  moddi  12778  uzrdgfni  12797  axdc4uzlem  12822  seqf1olem1  12880  seqf1olem2  12881  seqid2  12887  expnegz  12934  binom2sub  13021  binom3  13025  hashreshashfun  13264  wrdlenccats1lenm1OLD  13441  ccatw2s1p2  13459  ccats1swrdeq  13515  swrdccatin12lem2  13535  swrdccatin12  13537  swrdccat3b  13542  cshweqrep  13613  2cshwcshw  13617  ccatco  13627  swrds2  13731  relexpsucnnr  13809  relexpaddnn  13835  reim  13893  mulre  13905  addcj  13932  absimle  14093  clim2ser  14429  isercoll2  14443  serf0  14455  iseralt  14459  summolem3  14489  isumclim3  14534  mptfzshft  14554  fsumrev  14555  fsum2mul  14565  incexc  14613  isumsplit  14616  mertenslem1  14660  fprodrev  14751  iprodclim3  14775  binomfallfaclem2  14815  ef4p  14887  tanval3  14908  efival  14926  sinmul  14946  bitsinvp1  15218  sadaddlem  15235  bitsshft  15244  smu01lem  15254  dfgcd2  15310  lcmgcdlem  15366  lcm1  15370  lcmfass  15406  eulerthlem2  15534  hashgcdeq  15541  powm2modprm  15555  pythagtriplem16  15582  pczpre  15599  pcqdiv  15609  pcadd  15640  pcfac  15650  prmreclem5  15671  4sqlem10  15698  4sqlem19  15714  vdwapun  15725  vdwlem1  15732  ramcl  15780  setsstruct  15945  strfvd  15951  strfv2d  15952  xpsff1o  16275  xpslem  16280  2oppccomf  16432  oppcepi  16446  sscfn1  16524  sscfn2  16525  invfuc  16681  funcestrcsetclem7  16833  funcsetcestrclem7  16848  grpinvssd  17539  grpinvval2  17545  pmtrdifwrdellem2  17948  psgnunilem1  17959  psgnuni  17965  pgp0  18057  sylow1lem1  18059  sylow3lem2  18089  efgredleme  18202  efgcpbllemb  18214  frgpuptinv  18230  frgpup3lem  18236  gexexlem  18301  cyggenod  18332  gsumval3eu  18351  gsumval3  18354  gsumzaddlem  18367  dprd2db  18488  ringinvdv  18740  lss1d  19011  pwssplit1  19107  mplcoe3  19514  subrgascl  19546  evlseu  19564  ply1sclid  19706  znzrh2  19942  regsumsupp  20016  ipassr2  20040  dsmmfi  20130  frlmlss  20143  frlmip  20165  frlmlbs  20184  frlmup3  20187  islindf4  20225  1marepvmarrepid  20429  madurid  20498  smadiadetlem3  20522  mat2pmatghm  20583  pmatcollpwscmatlem1  20642  pm2mpmhmlem2  20672  cpmadurid  20720  cpmidgsumm2pm  20722  cpmadugsumlemB  20727  cayhamlem2  20737  ntrval2  20903  ordtuni  21042  cnclima  21120  cmpsub  21251  ptbasfi  21432  txbasval  21457  pt1hmeo  21657  alexsubALTlem1  21898  trust  22080  ussid  22111  ressuss  22114  ressprdsds  22223  imasdsf1olem  22225  setsms  22332  tmsxms  22338  tmsxpsmopn  22389  subgnm  22484  tngnm  22502  tngngp2  22503  xrsxmet  22659  xrge0gsumle  22683  metdstri  22701  xrhmeo  22792  lebnumlem3  22809  pcorevlem  22872  pi1xfrcnvlem  22902  clmabs  22929  cvsmuleqdivd  22980  rrxip  23224  rrxds  23227  minveclem4a  23247  pjthlem1  23254  divcncf  23262  ovolunlem1a  23310  mbfres2  23457  i1faddlem  23505  ibladdlem  23631  iblabs  23640  ditgsplit  23670  dvnres  23739  dvmptdiv  23782  dveflem  23787  dveq0  23808  dvfsumabs  23831  itgsubstlem  23856  ply1divex  23941  dgrco  24076  plycjlem  24077  taylthlem1  24172  pserdv2  24229  abelthlem6  24235  abelthlem7  24237  tangtx  24302  abssinper  24315  sineq0  24318  explog  24385  reexplog  24386  eflogeq  24393  abslogle  24409  tanarg  24410  logtayl  24451  logtayl2  24453  relogbdiv  24562  ang180lem3  24586  affineequiv  24598  affineequiv2  24599  chordthmlem4  24607  chordthmlem5  24608  heron  24610  dcubic1lem  24615  dcubic2  24616  dcubic  24618  mcubic  24619  cubic2  24620  dquartlem1  24623  dquart  24625  quart1lem  24627  quartlem1  24629  quart  24633  acoscos  24665  atanlogaddlem  24685  atantayl2  24710  atantayl3  24711  birthdaylem2  24724  efrlim  24741  amgmlem  24761  logdifbnd  24765  emcllem3  24769  emcllem6  24772  lgamgulmlem2  24801  lgamgulmlem3  24802  lgamgulmlem4  24803  lgamgulmlem5  24804  gamigam  24824  lgamcvg2  24826  gamfac  24838  basellem3  24854  basellem8  24859  basellem9  24860  chtprm  24924  logfaclbnd  24992  perfect1  24998  bcp1ctr  25049  bclbnd  25050  bposlem1  25054  lgsdilem  25094  lgsdirnn0  25114  lgsdinn0  25115  gausslemma2dlem1a  25135  gausslemma2dlem4  25139  gausslemma2dlem5a  25140  lgseisenlem2  25146  lgsquadlem1  25150  2sqlem2  25188  mul2sq  25189  vmadivsum  25216  rpvmasumlem  25221  dchrisumlem1  25223  dchrisumlem2  25224  dchrmusum2  25228  dchrvmasum2if  25231  dchrisum0lem2  25252  logsqvma2  25277  selberg3  25293  selberg4lem1  25294  pntrsumo1  25299  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntibndlem2  25325  pntlemk  25340  pntlemo  25341  ostth2lem4  25370  ostth3  25372  tgbtwndiff  25446  tgifscgr  25448  trgcgrg  25455  motcgr3  25485  tgbtwnconn1lem1  25512  tgbtwnconn1lem2  25513  ismir  25599  miriso  25610  midexlem  25632  ragmir  25640  footex  25658  colperpexlem3  25669  mideulem2  25671  midex  25674  opphllem3  25686  midcgr  25717  lmiisolem  25733  brbtwn2  25830  colinearalglem4  25834  axsegconlem1  25842  axpaschlem  25865  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  ushgredgedgloop  26168  crctcshwlkn0lem6  26763  wwlknlsw  26796  wwlksnextwrd  26860  clwlkclwwlklem2a3  26960  clwlkclwwlk2  26969  clwwlkel  27009  clwwlkfo  27013  clwwlkext2edg  27020  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  eupth2eucrct  27195  numclwwlk2lem1lem  27324  numclwwlk2lem1lemOLD  27325  clwwlkccatlem  27331  numclwlk1lem2fo  27348  numclwlk2lem2f  27357  numclwlk2lem2fOLD  27364  grpoidinvlem2  27487  nvmtri  27654  cnnvm  27665  nvnd  27671  ipidsq  27693  ipnm  27694  ipipcj  27698  blocnilem  27787  ipasslem2  27815  dipsubdir  27831  hvaddsubval  28018  pjhthlem1  28378  pjspansn  28564  pjo  28658  unoplin  28907  adjadj  28923  hmoplin  28929  eigvec1  28949  lnopeqi  28995  nmcexi  29013  lnfnsubi  29033  riesz3i  29049  kbass6  29108  leoprf2  29114  leoprf  29115  pjnmopi  29135  mdslmd1lem1  29312  mdslmd1lem2  29313  superpos  29341  ifeq3da  29491  fgreu  29599  resf1o  29633  fprodex01  29699  2sqmod  29776  gsummpt2d  29909  xrge0tsmseq  29915  subrgchr  29922  rhmdvd  29949  symgfcoeu  29973  psgnfzto1stlem  29978  psgnfzto1st  29983  madjusmdetlem2  30022  qtophaus  30031  pstmval  30066  mndpluscn  30100  qqhucn  30164  esumval  30236  gsumesum  30249  esumcst  30253  esumpcvgval  30268  oddpwdc  30544  eulerpartlemgvv  30566  probdif  30610  sgnmul  30732  signsvtn  30789  actfunsnf1o  30810  reprpmtf1o  30832  hgt750lemd  30854  logdivsqrle  30856  hgt750lemg  30860  hgt750lemb  30862  bnj1415  31232  derangen2  31282  subfaclefac  31284  subfaclim  31296  mrsubrn  31536  sinccvglem  31692  bcprod  31750  filnetlem4  32501  curunc  33521  ltflcei  33527  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  mblfinlem4  33579  ibladdnclem  33596  iblabsnc  33604  iblmulc2nc  33605  ftc1anclem6  33620  ftc1anclem8  33622  sdclem2  33668  ismtycnv  33731  heiborlem10  33749  lflvsass  34686  lkrscss  34703  eqlkr  34704  eqlkr3  34706  ldualvsdi2  34749  omllaw3  34850  cmtcomlemN  34853  cmtbr3N  34859  omlfh3N  34864  llnexchb2lem  35472  dalawlem7  35481  dalawlem11  35485  dalawlem12  35486  pol1N  35514  paddatclN  35553  4atexlemcnd  35676  ltrncoidN  35732  cdleme3b  35834  cdleme11  35875  cdleme15a  35879  cdleme22e  35949  cdleme22g  35953  cdlemg18b  36284  trlcoat  36328  cdlemk2  36437  cdlemk4  36439  cdlemki  36446  cdlemksv2  36452  cdlemk15  36460  cdlemk55a  36564  diainN  36663  dia2dimlem3  36672  dia2dimlem5  36674  dvhlveclem  36714  diaocN  36731  cdlemn4  36804  cdlemn8  36810  dihopelvalcpre  36854  dihmeetlem9N  36921  dih1dimatlem  36935  dihpN  36942  dochvalr3  36969  dochsat  36989  djhjlj  37009  dochdmm1  37016  dihjatcclem4  37027  dihjat1  37035  dihjat4  37039  dochsnkr2cl  37080  dochfl1  37082  lclkrlem2j  37122  mapdordlem2  37243  mapdrvallem2  37251  hdmap10  37449  mzpsubmpt  37623  irrapxlem3  37705  pellexlem6  37715  pell1234qrne0  37734  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell14qrdich  37750  pell1qrgaplem  37754  rmxluc  37818  rmyluc  37819  jm2.24nn  37843  jm2.18  37872  jm2.19lem2  37874  jm2.19lem3  37875  jm2.22  37879  jm2.23  37880  jm2.16nn0  37888  jm2.27c  37891  fnwe2lem2  37938  lmhmfgsplit  37973  hbtlem2  38011  relexpmulnn  38318  relexpmulg  38319  ntrclsneine0lem  38679  int-addassocd  38794  dvconstbi  38850  bccm1k  38858  binomcxplemnotnn0  38872  fmptsnxp  39663  wessf1ornlem  39685  founiiun0  39691  disjinfi  39694  projf1o  39700  infnsuprnmpt  39779  lefldiveq  39819  lt4addmuld  39834  fzdifsuc2  39838  suplesup  39868  infrpge  39880  xrlexaddrp  39881  xralrple2  39883  infleinflem1  39899  supminfrnmpt  39985  supminfxr2  40012  fsumnncl  40121  limcperiod  40178  sumnnodd  40180  limcresiooub  40192  limcresioolb  40193  0ellimcdiv  40199  reclimc  40203  limsupval3  40242  limsupequzmpt2  40268  liminfval5  40315  limsupresxr  40316  liminfresxr  40317  liminfvalxr  40333  liminfequzmpt2  40341  climliminflimsupd  40351  liminfltlem  40354  sinmulcos  40394  coskpi2  40395  cncfdmsn  40421  cncfiooicclem1  40424  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  fperdvper  40451  dvmptresicc  40452  dvnmptdivc  40471  dvnxpaek  40475  dvnmul  40476  dvnprodlem1  40479  dvnprodlem3  40481  itgcoscmulx  40503  itgsincmulx  40508  itgspltprt  40513  itgiccshift  40514  itgperiod  40515  sublevolico  40519  volioof  40522  ovolsplit  40523  fvvolioof  40524  fvvolicof  40526  stoweidlem22  40557  stoweidlem32  40567  wallispilem5  40604  stirlinglem5  40613  dirkertrigeqlem2  40634  dirkertrigeq  40636  dirkercncflem1  40638  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem13  40655  fourierdlem16  40658  fourierdlem19  40661  fourierdlem21  40663  fourierdlem22  40664  fourierdlem28  40670  fourierdlem32  40674  fourierdlem33  40675  fourierdlem42  40684  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem56  40697  fourierdlem60  40701  fourierdlem61  40702  fourierdlem64  40705  fourierdlem66  40707  fourierdlem71  40712  fourierdlem73  40714  fourierdlem74  40715  fourierdlem76  40717  fourierdlem78  40719  fourierdlem79  40720  fourierdlem80  40721  fourierdlem81  40722  fourierdlem83  40724  fourierdlem88  40729  fourierdlem92  40733  fourierdlem93  40734  fourierdlem97  40738  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem109  40750  fourierdlem111  40752  fouriersw  40766  elaa2lem  40768  etransclem24  40793  etransclem25  40794  etransclem35  40804  etransclem46  40815  rrxdsfi  40823  rrndistlt  40828  rrxunitopnfi  40830  qndenserrnbl  40833  qndenserrnopnlem  40835  saldifcl2  40864  intsal  40866  sge0sn  40914  sge0ltfirp  40935  sge0iunmptlemre  40950  sge0fodjrnlem  40951  sge0isum  40962  sge0xaddlem1  40968  nnfoctbdjlem  40990  meassle  40998  ismeannd  41002  meadif  41014  meaiuninclem  41015  meaiininclem  41021  omeunile  41040  caragendifcl  41049  caratheodory  41063  isomenndlem  41065  ovnsubaddlem1  41105  hoidmv1lelem2  41127  hoidmv1le  41129  hoidmvlelem2  41131  hoidmvle  41135  hoi2toco  41142  rrnmbl  41149  hoidifhspdmvle  41155  voncmpl  41156  hoiqssbl  41160  hspmbllem1  41161  hspmbllem2  41162  ovolval2lem  41178  ovolval5lem2  41188  ovnovollem1  41191  ovnovollem2  41192  hoimbl2  41200  vonhoire  41207  salpreimagelt  41239  salpreimalegt  41241  preimaioomnf  41250  smfres  41318  smfmullem1  41319  smflimmpt  41337  smfsupmpt  41342  smfinfmpt  41346  smflimsupmpt  41356  smfliminflem  41357  smfliminfmpt  41359  sigarcol  41374  ccats1pfxeq  41746  pfxccatin12lem2  41749  pfxccatin12  41750  sfprmdvdsmersenne  41845  lighneallem3  41849  lighneallem4  41852  nn0onn0exALTV  41934  nnsum3primesprm  42003  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  elsprel  42050  c0snmgmhm  42239  rngcifuestrc  42322  funcrngcsetc  42323  funcrngcsetcALT  42324  funcringcsetc  42360  funcringcsetcALTV2lem7  42367  funcringcsetclem7ALTV  42390  lincext3  42570  lincresunit3  42595  nn0onn0ex  42643  nnpw2pmod  42702  blennn0em1  42710  digexp  42726  dignn0ehalf  42736  nn0mulfsum  42743  recsec  42825  reccsc  42826  aacllem  42875  amgmlemALT  42877
  Copyright terms: Public domain W3C validator