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

Theorem eqtr2d 2656
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 2655 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2627 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614
This theorem is referenced by:  3eqtrrd  2660  3eqtr2rd  2662  ifan  4112  ifor  4113  dfopif  4374  nvocnv  6502  elovmpt3rab1  6858  onsucmin  6983  csbopeq1a  7181  oaabs2  7685  ecinxp  7782  resixpfo  7906  sbthlem3  8032  rankxpsuc  8705  fseqenlem2  8808  dfac2  8913  isf32lem9  9143  compsscnvlem  9152  ttukeylem7  9297  fpwwe2lem11  9422  00id  10171  submul2  10430  mulsubfacd  10452  divadddiv  10700  infrenegsup  10966  xadd4d  12092  fzdifsuc  12358  fzval3  12493  fzoshftral  12541  ceim1l  12602  fldiv  12615  flmod  12640  intfrac  12641  modcyc2  12662  moddi  12694  uzrdgfni  12713  axdc4uzlem  12738  seqf1olem1  12796  seqf1olem2  12797  seqid2  12803  expnegz  12850  binom2sub  12937  binom3  12941  wrdlenccats1lenm1  13354  ccatw2s1p2  13368  ccats1swrdeq  13423  swrdccatin12lem2  13442  swrdccatin12  13444  swrdccat3b  13449  cshweqrep  13520  2cshwcshw  13524  ccatco  13534  swrds2  13635  relexpsucnnr  13715  relexpaddnn  13741  reim  13799  mulre  13811  addcj  13838  absimle  13999  clim2ser  14335  isercoll2  14349  serf0  14361  iseralt  14365  summolem3  14394  isumclim3  14437  mptfzshft  14457  fsumrev  14458  fsum2mul  14468  incexc  14513  isumsplit  14516  mertenslem1  14560  fprodrev  14651  iprodclim3  14675  binomfallfaclem2  14715  ef4p  14787  tanval3  14808  efival  14826  sinmul  14846  bitsinvp1  15114  sadaddlem  15131  bitsshft  15140  smu01lem  15150  dfgcd2  15206  lcmgcdlem  15262  lcm1  15266  lcmfass  15302  eulerthlem2  15430  hashgcdeq  15437  powm2modprm  15451  pythagtriplem16  15478  pczpre  15495  pcqdiv  15505  pcadd  15536  pcfac  15546  prmreclem5  15567  4sqlem10  15594  4sqlem19  15610  vdwapun  15621  vdwlem1  15628  ramcl  15676  setsstruct  15838  strfvd  15844  strfv2d  15845  xpsff1o  16168  xpslem  16173  2oppccomf  16325  oppcepi  16339  sscfn1  16417  sscfn2  16418  invfuc  16574  funcestrcsetclem7  16726  funcsetcestrclem7  16741  grpinvssd  17432  grpinvval2  17438  pmtrdifwrdellem2  17842  psgnunilem1  17853  psgnuni  17859  pgp0  17951  sylow1lem1  17953  sylow3lem2  17983  efgredleme  18096  efgcpbllemb  18108  frgpuptinv  18124  frgpup3lem  18130  gexexlem  18195  cyggenod  18226  gsumval3eu  18245  gsumval3  18248  gsumzaddlem  18261  dprd2db  18382  ringinvdv  18634  lss1d  18903  pwssplit1  18999  mplcoe3  19406  subrgascl  19438  evlseu  19456  ply1sclid  19598  znzrh2  19834  regsumsupp  19908  ipassr2  19932  dsmmfi  20022  frlmlss  20035  frlmip  20057  frlmlbs  20076  frlmup3  20079  islindf4  20117  1marepvmarrepid  20321  madurid  20390  smadiadetlem3  20414  mat2pmatghm  20475  pmatcollpwscmatlem1  20534  pm2mpmhmlem2  20564  cpmadurid  20612  cpmidgsumm2pm  20614  cpmadugsumlemB  20619  cayhamlem2  20629  ntrval2  20795  ordtuni  20934  cnclima  21012  cmpsub  21143  ptbasfi  21324  txbasval  21349  pt1hmeo  21549  alexsubALTlem1  21791  trust  21973  ussid  22004  ressuss  22007  ressprdsds  22116  imasdsf1olem  22118  setsms  22225  tmsxms  22231  tmsxpsmopn  22282  subgnm  22377  tngnm  22395  tngngp2  22396  xrsxmet  22552  xrge0gsumle  22576  metdstri  22594  xrhmeo  22685  lebnumlem3  22702  pcorevlem  22766  pi1xfrcnvlem  22796  clmabs  22823  cvsmuleqdivd  22874  rrxip  23118  rrxds  23121  minveclem4a  23141  pjthlem1  23148  divcncf  23156  ovolunlem1a  23204  mbfres2  23352  i1faddlem  23400  ibladdlem  23526  iblabs  23535  ditgsplit  23565  dvnres  23634  dveflem  23680  dveq0  23701  dvfsumabs  23724  itgsubstlem  23749  ply1divex  23834  dgrco  23969  plycjlem  23970  taylthlem1  24065  pserdv2  24122  abelthlem6  24128  abelthlem7  24130  tangtx  24195  abssinper  24208  sineq0  24211  explog  24278  reexplog  24279  eflogeq  24286  abslogle  24302  tanarg  24303  logtayl  24340  logtayl2  24342  relogbdiv  24451  ang180lem3  24475  affineequiv  24487  affineequiv2  24488  chordthmlem4  24496  chordthmlem5  24497  heron  24499  dcubic1lem  24504  dcubic2  24505  dcubic  24507  mcubic  24508  cubic2  24509  dquartlem1  24512  dquart  24514  quart1lem  24516  quartlem1  24518  quart  24522  acoscos  24554  atanlogaddlem  24574  atantayl2  24599  atantayl3  24600  birthdaylem2  24613  efrlim  24630  amgmlem  24650  logdifbnd  24654  emcllem3  24658  emcllem6  24661  lgamgulmlem2  24690  lgamgulmlem3  24691  lgamgulmlem4  24692  lgamgulmlem5  24693  gamigam  24713  lgamcvg2  24715  gamfac  24727  basellem3  24743  basellem8  24748  basellem9  24749  chtprm  24813  logfaclbnd  24881  perfect1  24887  bcp1ctr  24938  bclbnd  24939  bposlem1  24943  lgsdilem  24983  lgsdirnn0  25003  lgsdinn0  25004  gausslemma2dlem1a  25024  gausslemma2dlem4  25028  gausslemma2dlem5a  25029  lgseisenlem2  25035  lgsquadlem1  25039  2sqlem2  25077  mul2sq  25078  vmadivsum  25105  rpvmasumlem  25110  dchrisumlem1  25112  dchrisumlem2  25113  dchrmusum2  25117  dchrvmasum2if  25120  dchrisum0lem2  25141  logsqvma2  25166  selberg3  25182  selberg4lem1  25183  pntrsumo1  25188  pntrlog2bndlem2  25201  pntrlog2bndlem3  25202  pntrlog2bndlem5  25204  pntibndlem2  25214  pntlemk  25229  pntlemo  25230  ostth2lem4  25259  ostth3  25261  tgbtwndiff  25335  tgifscgr  25337  trgcgrg  25344  motcgr3  25374  tgbtwnconn1lem1  25401  tgbtwnconn1lem2  25402  ismir  25488  miriso  25499  midexlem  25521  ragmir  25529  footex  25547  colperpexlem3  25558  mideulem2  25560  midex  25563  opphllem3  25575  midcgr  25606  lmiisolem  25622  brbtwn2  25719  colinearalglem4  25723  axsegconlem1  25731  axpaschlem  25754  axcontlem4  25781  axcontlem7  25784  axcontlem8  25785  ushgredgedgloop  26050  crctcshwlkn0lem6  26610  wwlksnextwrd  26695  clwlkclwwlklem2a3  26796  clwlkclwwlk2  26805  clwwlksel  26814  clwwlksfo  26818  clwwlksext2edg  26823  wwlksext2clwwlk  26824  eupth2eucrct  26977  clwwlkextfrlem1  27101  numclwlk1lem2foa  27113  numclwlk1lem2fo  27117  numclwlk2lem2f  27125  grpoidinvlem2  27247  nvmtri  27414  cnnvm  27425  nvnd  27431  ipidsq  27453  ipnm  27454  ipipcj  27458  blocnilem  27547  ipasslem2  27575  dipsubdir  27591  hvaddsubval  27778  pjhthlem1  28138  pjspansn  28324  pjo  28418  unoplin  28667  adjadj  28683  hmoplin  28689  eigvec1  28709  lnopeqi  28755  nmcexi  28773  lnfnsubi  28793  riesz3i  28809  kbass6  28868  leoprf2  28874  leoprf  28875  pjnmopi  28895  mdslmd1lem1  29072  mdslmd1lem2  29073  superpos  29101  fgreu  29355  resf1o  29389  2sqmod  29475  gsummpt2d  29608  xrge0tsmseq  29614  subrgchr  29621  rhmdvd  29648  symgfcoeu  29672  psgnfzto1stlem  29677  psgnfzto1st  29682  madjusmdetlem2  29718  qtophaus  29727  pstmval  29762  mndpluscn  29796  qqhucn  29860  esumval  29931  gsumesum  29944  esumcst  29948  esumpcvgval  29963  oddpwdc  30239  eulerpartlemgvv  30261  probdif  30305  sgnmul  30427  signsvtn  30483  bnj1415  30867  derangen2  30917  subfaclefac  30919  subfaclim  30931  mrsubrn  31171  sinccvglem  31327  bcprod  31385  filnetlem4  32071  curunc  33062  ltflcei  33068  matunitlindflem1  33076  matunitlindflem2  33077  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem24  33104  mblfinlem4  33120  ibladdnclem  33137  iblabsnc  33145  iblmulc2nc  33146  ftc1anclem6  33161  ftc1anclem8  33163  sdclem2  33209  ismtycnv  33272  heiborlem10  33290  lflvsass  33887  lkrscss  33904  eqlkr  33905  eqlkr3  33907  ldualvsdi2  33950  omllaw3  34051  cmtcomlemN  34054  cmtbr3N  34060  omlfh3N  34065  llnexchb2lem  34673  dalawlem7  34682  dalawlem11  34686  dalawlem12  34687  pol1N  34715  paddatclN  34754  4atexlemcnd  34877  ltrncoidN  34933  cdleme3b  35035  cdleme11  35076  cdleme15a  35080  cdleme22e  35151  cdleme22g  35155  cdlemg18b  35486  trlcoat  35530  cdlemk2  35639  cdlemk4  35641  cdlemki  35648  cdlemksv2  35654  cdlemk15  35662  cdlemk55a  35766  diainN  35865  dia2dimlem3  35874  dia2dimlem5  35876  dvhlveclem  35916  diaocN  35933  cdlemn4  36006  cdlemn8  36012  dihopelvalcpre  36056  dihmeetlem9N  36123  dih1dimatlem  36137  dihpN  36144  dochvalr3  36171  dochsat  36191  djhjlj  36211  dochdmm1  36218  dihjatcclem4  36229  dihjat1  36237  dihjat4  36241  dochsnkr2cl  36282  dochfl1  36284  lclkrlem2j  36324  mapdordlem2  36445  mapdrvallem2  36453  hdmap10  36651  mzpsubmpt  36825  irrapxlem3  36907  pellexlem6  36917  pell1234qrne0  36936  pell1234qrreccl  36937  pell1234qrmulcl  36938  pell14qrdich  36952  pell1qrgaplem  36956  rmxluc  37020  rmyluc  37021  jm2.24nn  37045  jm2.18  37074  jm2.19lem2  37076  jm2.19lem3  37077  jm2.22  37081  jm2.23  37082  jm2.16nn0  37090  jm2.27c  37093  fnwe2lem2  37140  lmhmfgsplit  37175  hbtlem2  37214  relexpmulnn  37521  relexpmulg  37522  ntrclsneine0lem  37883  int-addassocd  37998  dvconstbi  38054  bccm1k  38062  binomcxplemnotnn0  38076  fmptsnxp  38858  wessf1ornlem  38880  founiiun0  38886  disjinfi  38889  projf1o  38895  infnsuprnmpt  38976  lefldiveq  39004  lt4addmuld  39019  fzdifsuc2  39024  suplesup  39054  infrpge  39066  xrlexaddrp  39067  xralrple2  39069  infleinflem1  39085  fsumnncl  39239  limcperiod  39296  sumnnodd  39298  limcresiooub  39310  limcresioolb  39311  0ellimcdiv  39317  reclimc  39321  limsupval3  39360  limsupequzmpt2  39386  sinmulcos  39411  coskpi2  39412  cncfdmsn  39438  cncfiooicclem1  39441  fprodsubrecnncnvlem  39456  fprodaddrecnncnvlem  39458  dvmptdiv  39469  fperdvper  39470  dvmptresicc  39471  dvnmptdivc  39490  dvnxpaek  39494  dvnmul  39495  dvnprodlem1  39498  dvnprodlem3  39500  itgcoscmulx  39522  itgsincmulx  39527  itgspltprt  39532  itgiccshift  39533  itgperiod  39534  sublevolico  39538  volioof  39541  ovolsplit  39542  fvvolioof  39543  fvvolicof  39545  stoweidlem22  39576  stoweidlem32  39586  wallispilem5  39623  stirlinglem5  39632  dirkertrigeqlem2  39653  dirkertrigeq  39655  dirkercncflem1  39657  dirkercncflem2  39658  dirkercncflem4  39660  fourierdlem13  39674  fourierdlem16  39677  fourierdlem19  39680  fourierdlem21  39682  fourierdlem22  39683  fourierdlem28  39689  fourierdlem32  39693  fourierdlem33  39694  fourierdlem42  39703  fourierdlem47  39707  fourierdlem48  39708  fourierdlem49  39709  fourierdlem50  39710  fourierdlem56  39716  fourierdlem60  39720  fourierdlem61  39721  fourierdlem64  39724  fourierdlem66  39726  fourierdlem71  39731  fourierdlem73  39733  fourierdlem74  39734  fourierdlem76  39736  fourierdlem78  39738  fourierdlem79  39739  fourierdlem80  39740  fourierdlem81  39741  fourierdlem83  39743  fourierdlem88  39748  fourierdlem92  39752  fourierdlem93  39753  fourierdlem97  39757  fourierdlem101  39761  fourierdlem103  39763  fourierdlem104  39764  fourierdlem109  39769  fourierdlem111  39771  fouriersw  39785  elaa2lem  39787  etransclem24  39812  etransclem25  39813  etransclem35  39823  etransclem46  39834  rrxdsfi  39842  rrndistlt  39847  rrxunitopnfi  39849  qndenserrnbl  39852  qndenserrnopnlem  39854  saldifcl2  39883  intsal  39885  sge0sn  39933  sge0ltfirp  39954  sge0iunmptlemre  39969  sge0fodjrnlem  39970  sge0isum  39981  sge0xaddlem1  39987  nnfoctbdjlem  40009  meassle  40017  ismeannd  40021  meadif  40033  meaiuninclem  40034  meaiininclem  40037  omeunile  40056  caragendifcl  40065  caratheodory  40079  isomenndlem  40081  ovnsubaddlem1  40121  hoidmv1lelem2  40143  hoidmv1le  40145  hoidmvlelem2  40147  hoidmvle  40151  hoi2toco  40158  rrnmbl  40165  hoidifhspdmvle  40171  voncmpl  40172  hoiqssbl  40176  hspmbllem1  40177  hspmbllem2  40178  ovolval2lem  40194  ovolval5lem2  40204  ovnovollem1  40207  ovnovollem2  40208  hoimbl2  40216  vonhoire  40223  salpreimagelt  40255  salpreimalegt  40257  preimaioomnf  40266  smfres  40334  smfmullem1  40335  smflimmpt  40353  smfsupmpt  40358  smfinfmpt  40362  smflimsupmpt  40372  sigarcol  40387  ccats1pfxeq  40750  pfxccatin12lem2  40753  pfxccatin12  40754  sfprmdvdsmersenne  40849  lighneallem3  40853  lighneallem4  40856  nn0onn0exALTV  40938  nnsum3primesprm  40997  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  elsprel  41043  c0snmgmhm  41232  rngcifuestrc  41315  funcrngcsetc  41316  funcrngcsetcALT  41317  funcringcsetc  41353  funcringcsetcALTV2lem7  41360  funcringcsetclem7ALTV  41383  lincext3  41563  lincresunit3  41588  nn0onn0ex  41636  nnpw2pmod  41699  blennn0em1  41707  digexp  41723  dignn0ehalf  41733  nn0mulfsum  41740  recsec  41820  reccsc  41821  aacllem  41880  amgmlemALT  41882
  Copyright terms: Public domain W3C validator