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

Theorem eqtr2d 2852
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 2851 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2823 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2810
This theorem is referenced by:  3eqtrrd  2856  3eqtr2rd  2858  ifan  4341  ifor  4342  dfopif  4603  nvocnv  6771  elovmpt3rab1  7133  onsucmin  7261  csbopeq1a  7463  oaabs2  7972  ecinxp  8067  resixpfo  8193  sbthlem3  8321  rankxpsuc  9002  fseqenlem2  9141  dfac2b  9246  dfac2OLD  9248  isf32lem9  9478  compsscnvlem  9487  ttukeylem7  9632  fpwwe2lem11  9757  00id  10506  submul2  10765  mulsubfacd  10787  divadddiv  11035  infrenegsup  11301  xadd4d  12371  fzdifsuc  12643  fzval3  12781  fzoshftral  12829  ceim1l  12890  fldiv  12903  flmod  12928  intfrac  12929  modcyc2  12950  moddi  12982  uzrdgfni  13001  axdc4uzlem  13026  seqf1olem1  13083  seqf1olem2  13084  seqid2  13090  expnegz  13137  binom2sub  13224  binom3  13228  hashreshashfun  13463  wrdlenccats1lenm1OLD  13639  ccatw2s1p2  13657  ccats1swrdeq  13713  swrdccatin12lem2  13733  swrdccatin12  13735  swrdccat3b  13740  cshweqrep  13811  2cshwcshw  13815  ccatco  13825  swrds2  13929  relexpsucnnr  14008  relexpaddnn  14034  reim  14092  mulre  14104  addcj  14131  absimle  14292  clim2ser  14628  isercoll2  14642  serf0  14654  iseralt  14658  summolem3  14688  isumclim3  14733  mptfzshft  14752  fsumrev  14753  fsum2mul  14763  incexc  14811  isumsplit  14814  mertenslem1  14857  fprodrev  14948  iprodclim3  14971  binomfallfaclem2  15011  ef4p  15083  tanval3  15104  efival  15122  sinmul  15142  bitsinvp1  15410  sadaddlem  15427  bitsshft  15436  smu01lem  15446  dfgcd2  15502  lcmgcdlem  15558  lcm1  15562  lcmfass  15598  eulerthlem2  15724  hashgcdeq  15731  powm2modprm  15745  pythagtriplem16  15772  pczpre  15789  pcqdiv  15799  pcadd  15830  pcfac  15840  prmreclem5  15861  4sqlem10  15888  4sqlem19  15904  vdwapun  15915  vdwlem1  15922  ramcl  15970  setsstruct  16129  strfvd  16135  strfv2d  16136  xpsff1o  16453  xpslem  16458  2oppccomf  16609  oppcepi  16623  sscfn1  16701  sscfn2  16702  invfuc  16858  funcestrcsetclem7  17011  funcsetcestrclem7  17026  grpinvssd  17717  grpinvval2  17723  pmtrdifwrdellem2  18123  psgnunilem1  18134  psgnuni  18140  pgp0  18232  sylow1lem1  18234  sylow3lem2  18264  efgredleme  18377  efgcpbllemb  18389  frgpuptinv  18405  frgpup3lem  18411  gexexlem  18476  cyggenod  18507  gsumval3eu  18526  gsumval3  18529  gsumzaddlem  18542  dprd2db  18664  ringinvdv  18916  lss1d  19190  pwssplit1  19286  mplcoe3  19695  subrgascl  19726  evlseu  19744  ply1sclid  19886  znzrh2  20121  regsumsupp  20197  ipassr2  20222  dsmmfi  20313  frlmlss  20326  frlmip  20348  frlmlbs  20367  frlmup3  20370  islindf4  20408  1marepvmarrepid  20613  madurid  20682  smadiadetlem3  20707  mat2pmatghm  20769  pmatcollpwscmatlem1  20828  pm2mpmhmlem2  20858  cpmadurid  20906  cpmidgsumm2pm  20908  cpmadugsumlemB  20913  cayhamlem2  20923  ntrval2  21090  ordtuni  21229  cnclima  21307  cmpsub  21438  ptbasfi  21619  txbasval  21644  pt1hmeo  21844  alexsubALTlem1  22085  trust  22267  ussid  22298  ressuss  22301  ressprdsds  22410  imasdsf1olem  22412  setsms  22519  tmsxms  22525  tmsxpsmopn  22576  subgnm  22671  tngnm  22689  tngngp2  22690  xrsxmet  22846  xrge0gsumle  22870  metdstri  22888  xrhmeo  22979  lebnumlem3  22996  pcorevlem  23059  pi1xfrcnvlem  23089  clmabs  23116  cvsmuleqdivd  23167  rrxip  23413  rrxds  23416  minveclem4a  23436  pjthlem1  23443  divcncf  23451  ovolunlem1a  23500  mbfres2  23649  i1faddlem  23697  ibladdlem  23823  iblabs  23832  ditgsplit  23862  dvnres  23931  dvmptdiv  23974  dveflem  23979  dveq0  24000  dvfsumabs  24023  itgsubstlem  24048  ply1divex  24133  dgrco  24268  plycjlem  24269  taylthlem1  24364  pserdv2  24421  abelthlem6  24427  abelthlem7  24429  tangtx  24495  abssinper  24508  sineq0  24511  explog  24577  reexplog  24578  eflogeq  24585  abslogle  24601  tanarg  24602  logtayl  24643  logtayl2  24645  relogbdiv  24754  ang180lem3  24778  affineequiv  24790  affineequiv2  24791  chordthmlem4  24799  chordthmlem5  24800  heron  24802  dcubic1lem  24807  dcubic2  24808  dcubic  24810  mcubic  24811  cubic2  24812  dquartlem1  24815  dquart  24817  quart1lem  24819  quartlem1  24821  quart  24825  acoscos  24857  atanlogaddlem  24877  atantayl2  24902  atantayl3  24903  birthdaylem2  24916  efrlim  24933  amgmlem  24953  logdifbnd  24957  emcllem3  24961  emcllem6  24964  lgamgulmlem2  24993  lgamgulmlem3  24994  lgamgulmlem4  24995  lgamgulmlem5  24996  gamigam  25016  lgamcvg2  25018  gamfac  25030  basellem3  25046  basellem8  25051  basellem9  25052  chtprm  25116  logfaclbnd  25184  perfect1  25190  bcp1ctr  25241  bclbnd  25242  bposlem1  25246  lgsdilem  25286  lgsdirnn0  25306  lgsdinn0  25307  gausslemma2dlem1a  25327  gausslemma2dlem4  25331  gausslemma2dlem5a  25332  lgseisenlem2  25338  lgsquadlem1  25342  2sqlem2  25380  mul2sq  25381  vmadivsum  25408  rpvmasumlem  25413  dchrisumlem1  25415  dchrisumlem2  25416  dchrmusum2  25420  dchrvmasum2if  25423  dchrisum0lem2  25444  logsqvma2  25469  selberg3  25485  selberg4lem1  25486  pntrsumo1  25491  pntrlog2bndlem2  25504  pntrlog2bndlem3  25505  pntrlog2bndlem5  25507  pntibndlem2  25517  pntlemk  25532  pntlemo  25533  ostth2lem4  25562  ostth3  25564  tgbtwndiff  25638  tgifscgr  25640  trgcgrg  25647  motcgr3  25677  tgbtwnconn1lem1  25704  tgbtwnconn1lem2  25705  ismir  25791  miriso  25802  midexlem  25824  ragmir  25832  footex  25850  colperpexlem3  25861  mideulem2  25863  midex  25866  opphllem3  25878  midcgr  25909  lmiisolem  25925  brbtwn2  26022  colinearalglem4  26026  axsegconlem1  26034  axpaschlem  26057  axcontlem4  26084  axcontlem7  26087  axcontlem8  26088  ushgredgedgloop  26361  ushgredgedgloopOLD  26362  crctcshwlkn0lem6  26959  wwlknlsw  26992  wwlksnextwrd  27057  clwwlkccatlem  27155  clwlkclwwlklem2a3  27160  clwlkclwwlk2  27169  clwwlkel  27218  clwwlkfo  27222  clwwlkext2edg  27229  wwlksext2clwwlk  27230  wwlksext2clwwlkOLD  27231  eupth2eucrct  27413  numclwwlk2lem1lem  27541  numclwwlk2lem1lemOLD  27542  numclwwlk1lem2fo  27560  numclwlk2lem2f  27580  numclwlk2lem2fOLD  27587  grpoidinvlem2  27711  nvmtri  27877  cnnvm  27888  nvnd  27894  ipidsq  27916  ipnm  27917  ipipcj  27921  blocnilem  28010  ipasslem2  28038  dipsubdir  28054  hvaddsubval  28241  pjhthlem1  28601  pjspansn  28787  pjo  28881  unoplin  29130  adjadj  29146  hmoplin  29152  eigvec1  29172  lnopeqi  29218  nmcexi  29236  lnfnsubi  29256  riesz3i  29272  kbass6  29331  leoprf2  29337  leoprf  29338  pjnmopi  29358  mdslmd1lem1  29535  mdslmd1lem2  29536  superpos  29564  ifeq3da  29713  fgreu  29821  resf1o  29855  fprodex01  29921  2sqmod  29996  gsummpt2d  30129  xrge0tsmseq  30135  subrgchr  30142  rhmdvd  30169  symgfcoeu  30193  psgnfzto1stlem  30198  psgnfzto1st  30203  madjusmdetlem2  30242  qtophaus  30251  pstmval  30286  mndpluscn  30320  qqhucn  30384  esumval  30456  gsumesum  30469  esumcst  30473  esumpcvgval  30488  oddpwdc  30764  eulerpartlemgvv  30786  probdif  30830  sgnmul  30952  signsvtn  31009  actfunsnf1o  31030  reprpmtf1o  31052  hgt750lemd  31074  logdivsqrle  31076  hgt750lemg  31080  hgt750lemb  31082  bnj1415  31451  derangen2  31501  subfaclefac  31503  subfaclim  31515  mrsubrn  31755  sinccvglem  31910  bcprod  31968  filnetlem4  32719  curunc  33723  ltflcei  33729  matunitlindflem1  33737  matunitlindflem2  33738  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem24  33765  mblfinlem4  33781  ibladdnclem  33797  iblabsnc  33805  iblmulc2nc  33806  ftc1anclem6  33821  ftc1anclem8  33823  sdclem2  33868  ismtycnv  33931  heiborlem10  33949  lflvsass  34880  lkrscss  34897  eqlkr  34898  eqlkr3  34900  ldualvsdi2  34943  omllaw3  35044  cmtcomlemN  35047  cmtbr3N  35053  omlfh3N  35058  llnexchb2lem  35667  dalawlem7  35676  dalawlem11  35680  dalawlem12  35681  pol1N  35709  paddatclN  35748  4atexlemcnd  35871  ltrncoidN  35927  cdleme3b  36028  cdleme11  36069  cdleme15a  36073  cdleme22e  36143  cdleme22g  36147  cdlemg18b  36478  trlcoat  36522  cdlemk2  36631  cdlemk4  36633  cdlemki  36640  cdlemksv2  36646  cdlemk15  36654  cdlemk55a  36758  diainN  36856  dia2dimlem3  36865  dia2dimlem5  36867  dvhlveclem  36907  diaocN  36924  cdlemn4  36997  cdlemn8  37003  dihopelvalcpre  37047  dihmeetlem9N  37114  dih1dimatlem  37128  dihpN  37135  dochvalr3  37162  dochsat  37182  djhjlj  37202  dochdmm1  37209  dihjatcclem4  37220  dihjat1  37228  dihjat4  37232  dochsnkr2cl  37273  dochfl1  37275  lclkrlem2j  37315  mapdordlem2  37436  mapdrvallem2  37444  hdmap10  37639  mzpsubmpt  37826  irrapxlem3  37908  pellexlem6  37918  pell1234qrne0  37937  pell1234qrreccl  37938  pell1234qrmulcl  37939  pell14qrdich  37953  pell1qrgaplem  37957  rmxluc  38020  rmyluc  38021  jm2.24nn  38045  jm2.18  38074  jm2.19lem2  38076  jm2.19lem3  38077  jm2.22  38081  jm2.23  38082  jm2.16nn0  38090  jm2.27c  38093  fnwe2lem2  38140  lmhmfgsplit  38175  hbtlem2  38213  relexpmulnn  38519  relexpmulg  38520  ntrclsneine0lem  38880  int-addassocd  38995  dvconstbi  39051  bccm1k  39059  binomcxplemnotnn0  39073  fmptsnxp  39856  wessf1ornlem  39878  founiiun0  39884  disjinfi  39887  projf1o  39893  infnsuprnmpt  39966  lefldiveq  40005  lt4addmuld  40019  fzdifsuc2  40023  suplesup  40053  infrpge  40065  xrlexaddrp  40066  xralrple2  40068  infleinflem1  40084  supminfrnmpt  40169  supminfxr2  40196  fsumnncl  40301  limcperiod  40358  sumnnodd  40360  limcresiooub  40372  limcresioolb  40373  0ellimcdiv  40379  reclimc  40383  limsupval3  40422  limsupequzmpt2  40448  liminfval5  40495  limsupresxr  40496  liminfresxr  40497  liminfvalxr  40513  liminfequzmpt2  40521  climliminflimsupd  40531  liminfltlem  40534  sinmulcos  40574  coskpi2  40575  cncfdmsn  40601  cncfiooicclem1  40604  fprodsubrecnncnvlem  40619  fprodaddrecnncnvlem  40621  fperdvper  40631  dvmptresicc  40632  dvnmptdivc  40651  dvnxpaek  40655  dvnmul  40656  dvnprodlem1  40659  dvnprodlem3  40661  itgcoscmulx  40682  itgsincmulx  40687  itgspltprt  40692  itgiccshift  40693  itgperiod  40694  sublevolico  40698  volioof  40701  ovolsplit  40702  fvvolioof  40703  fvvolicof  40705  stoweidlem22  40736  stoweidlem32  40746  wallispilem5  40783  stirlinglem5  40792  dirkertrigeqlem2  40813  dirkertrigeq  40815  dirkercncflem1  40817  dirkercncflem2  40818  dirkercncflem4  40820  fourierdlem13  40834  fourierdlem16  40837  fourierdlem19  40840  fourierdlem21  40842  fourierdlem22  40843  fourierdlem28  40849  fourierdlem32  40853  fourierdlem33  40854  fourierdlem42  40863  fourierdlem47  40867  fourierdlem48  40868  fourierdlem49  40869  fourierdlem50  40870  fourierdlem56  40876  fourierdlem60  40880  fourierdlem61  40881  fourierdlem64  40884  fourierdlem66  40886  fourierdlem71  40891  fourierdlem73  40893  fourierdlem74  40894  fourierdlem76  40896  fourierdlem78  40898  fourierdlem79  40899  fourierdlem80  40900  fourierdlem81  40901  fourierdlem83  40903  fourierdlem88  40908  fourierdlem92  40912  fourierdlem93  40913  fourierdlem97  40917  fourierdlem101  40921  fourierdlem103  40923  fourierdlem104  40924  fourierdlem109  40929  fourierdlem111  40931  fouriersw  40945  elaa2lem  40947  etransclem24  40972  etransclem25  40973  etransclem35  40983  etransclem46  40994  rrxdsfi  41002  rrndistlt  41007  rrxunitopnfi  41009  qndenserrnbl  41012  qndenserrnopnlem  41014  saldifcl2  41043  intsal  41045  sge0sn  41093  sge0ltfirp  41114  sge0iunmptlemre  41129  sge0fodjrnlem  41130  sge0isum  41141  sge0xaddlem1  41147  nnfoctbdjlem  41169  meassle  41177  ismeannd  41181  meadif  41193  meaiuninclem  41194  meaiininclem  41200  omeunile  41219  caragendifcl  41228  caratheodory  41242  isomenndlem  41244  ovnsubaddlem1  41284  hoidmv1lelem2  41306  hoidmv1le  41308  hoidmvlelem2  41310  hoidmvle  41314  hoi2toco  41321  rrnmbl  41328  hoidifhspdmvle  41334  voncmpl  41335  hoiqssbl  41339  hspmbllem1  41340  hspmbllem2  41341  ovolval2lem  41357  ovolval5lem2  41367  ovnovollem1  41370  ovnovollem2  41371  hoimbl2  41379  vonhoire  41386  salpreimagelt  41418  salpreimalegt  41420  preimaioomnf  41429  smfres  41497  smfmullem1  41498  smflimmpt  41516  smfsupmpt  41521  smfinfmpt  41525  smflimsupmpt  41535  smfliminflem  41536  smfliminfmpt  41538  sigarcol  41553  f1oresf1o  41898  f1oresf1o2  41899  ccats1pfxeq  42014  pfxccatin12lem2  42017  pfxccatin12  42018  sfprmdvdsmersenne  42113  lighneallem3  42117  lighneallem4  42120  nn0onn0exALTV  42202  nnsum3primesprm  42271  nnsum4primesodd  42277  nnsum4primesoddALTV  42278  elsprel  42311  c0snmgmhm  42500  rngcifuestrc  42583  funcrngcsetc  42584  funcrngcsetcALT  42585  funcringcsetc  42621  funcringcsetcALTV2lem7  42628  funcringcsetclem7ALTV  42651  lincext3  42831  lincresunit3  42856  nn0onn0ex  42904  nnpw2pmod  42963  blennn0em1  42971  digexp  42987  dignn0ehalf  42997  nn0mulfsum  43004  recsec  43086  reccsc  43087  aacllem  43136  amgmlemALT  43138
  Copyright terms: Public domain W3C validator