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

Theorem eqtr2d 2780
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 2779 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2745 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731
This theorem is referenced by:  3eqtrrd  2784  3eqtr2rd  2786  ifan  4513  ifor  4514  dfopifOLD  4802  fnco  6558  fnsnfv  6856  nvocnv  7162  elovmpt3rab1  7538  onsucmin  7677  csbopeq1a  7900  oaabs2  8488  ecinxp  8590  fsetfocdm  8658  resixpfo  8733  sbthlem3  8881  rankxpsuc  9649  fseqenlem2  9790  dfac2b  9895  isf32lem9  10126  compsscnvlem  10135  ttukeylem7  10280  fpwwe2lem10  10405  00id  11159  submul2  11424  mulsubfacd  11445  divadddiv  11699  infrenegsup  11967  xadd4d  13046  fzdifsuc  13325  fzval3  13465  fzoshftral  13513  ceim1l  13576  fldiv  13589  flmod  13614  intfrac  13615  modcyc2  13636  moddi  13668  uzrdgfni  13687  axdc4uzlem  13712  seqf1olem1  13771  seqf1olem2  13772  seqid2  13778  expnegz  13826  binom2sub  13944  binom3  13948  hashreshashfun  14163  ccatw2s1p2  14357  ccats1pfxeq  14436  pfxccatin12lem2  14453  pfxccatin12  14455  swrdccat3b  14462  cshweqrep  14543  2cshwcshw  14547  ccatco  14557  swrds2  14662  relexpsucnnr  14745  relexpaddnn  14771  reim  14829  mulre  14841  addcj  14868  absimle  15030  clim2ser  15375  isercoll2  15389  serf0  15401  iseralt  15405  summolem3  15435  isumclim3  15480  mptfzshft  15499  fsumrev  15500  fsum2mul  15510  incexc  15558  isumsplit  15561  mertenslem1  15605  fprodrev  15696  iprodclim3  15719  binomfallfaclem2  15759  ef4p  15831  tanval3  15852  efival  15870  sinmul  15890  bitsinvp1  16165  sadaddlem  16182  bitsshft  16191  smu01lem  16201  dfgcd2  16263  lcmgcdlem  16320  lcm1  16324  lcmfass  16360  eulerthlem2  16492  hashgcdeq  16499  powm2modprm  16513  pythagtriplem16  16540  pczpre  16557  pcqdiv  16567  pcadd  16599  pcfac  16609  prmreclem5  16630  4sqlem10  16657  4sqlem19  16673  vdwapun  16684  vdwlem1  16691  ramcl  16739  setsstruct  16886  strfvd  16911  strfv2d  16912  xpsff1o  17287  xpsrnbas  17291  2oppccomf  17445  oppcepi  17460  sscfn1  17538  sscfn2  17539  invfuc  17701  funcestrcsetclem7  17872  funcsetcestrclem7  17887  gsumsplit1r  18380  grpinvssd  18661  grpinvval2  18667  cycsubggend  18833  pmtrdifwrdellem2  19099  psgnunilem1  19110  psgnuni  19116  pgp0  19210  sylow1lem1  19212  sylow3lem2  19242  efgredleme  19358  efgcpbllemb  19370  frgpuptinv  19386  frgpup3lem  19392  gexexlem  19462  cyggenod  19493  gsumval3eu  19514  gsumval3  19517  gsumzaddlem  19531  dprd2db  19655  ablsimpgfindlem1  19719  ringinvdv  19945  lss1d  20234  pwssplit1  20330  znzrh2  20762  regsumsupp  20836  ipassr2  20861  dsmmfi  20954  frlmlss  20967  frlmip  20994  frlmlbs  21013  frlmup3  21016  islindf4  21054  mplcoe3  21248  subrgascl  21283  evlseu  21302  ply1sclid  21468  1marepvmarrepid  21733  madurid  21802  smadiadetlem3  21826  mat2pmatghm  21888  pmatcollpwscmatlem1  21947  pm2mpmhmlem2  21977  cpmadurid  22025  cpmidgsumm2pm  22027  cpmadugsumlemB  22032  cayhamlem2  22042  ntrval2  22211  ordtuni  22350  cnclima  22428  cmpsub  22560  ptbasfi  22741  txbasval  22766  pt1hmeo  22966  alexsubALTlem1  23207  trust  23390  ussid  23421  ressuss  23423  ressprdsds  23533  imasdsf1olem  23535  setsms  23644  tmsxms  23651  tmsxpsmopn  23702  subgnm  23798  tngnm  23824  tngngp2  23825  xrsxmet  23981  xrge0gsumle  24005  metdstri  24023  xrhmeo  24118  lebnumlem3  24135  pcorevlem  24198  pi1xfrcnvlem  24228  clmabs  24255  cvsmuleqdivd  24306  rrxip  24563  rrxds  24566  rrxdsfi  24584  minveclem4a  24603  pjthlem1  24610  divcncf  24620  ovolunlem1a  24669  mbfres2  24818  i1faddlem  24866  ibladdlem  24993  iblabs  25002  ditgsplit  25034  dvmptresicc  25089  dvnres  25104  dvmptdiv  25147  dveflem  25152  dveq0  25173  dvfsumabs  25196  itgsubstlem  25221  ply1divex  25310  dgrco  25445  plycjlem  25446  taylthlem1  25541  pserdv2  25598  abelthlem6  25604  abelthlem7  25606  tangtx  25671  abssinper  25686  sineq0  25689  explog  25758  reexplog  25759  eflogeq  25766  abslogle  25782  tanarg  25783  logtayl  25824  logtayl2  25826  relogbdiv  25938  ang180lem3  25970  affineequiv  25982  affineequiv2  25983  chordthmlem4  25994  chordthmlem5  25995  heron  25997  dcubic1lem  26002  dcubic2  26003  dcubic  26005  mcubic  26006  cubic2  26007  dquartlem1  26010  dquart  26012  quart1lem  26014  quartlem1  26016  quart  26020  acoscos  26052  atanlogaddlem  26072  atantayl2  26097  atantayl3  26098  birthdaylem2  26111  efrlim  26128  amgmlem  26148  logdifbnd  26152  emcllem3  26156  emcllem6  26159  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  gamigam  26211  lgamcvg2  26213  gamfac  26225  basellem3  26241  basellem8  26246  basellem9  26247  chtprm  26311  logfaclbnd  26379  perfect1  26385  bcp1ctr  26436  bclbnd  26437  bposlem1  26441  lgsdilem  26481  lgsdirnn0  26501  lgsdinn0  26502  gausslemma2dlem1a  26522  gausslemma2dlem4  26526  gausslemma2dlem5a  26527  lgseisenlem2  26533  lgsquadlem1  26537  2sqlem2  26575  mul2sq  26576  2sqmod  26593  2sqnn0  26595  vmadivsum  26639  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasum2if  26654  dchrisum0lem2  26675  logsqvma2  26700  selberg3  26716  selberg4lem1  26717  pntrsumo1  26722  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem5  26738  pntibndlem2  26748  pntlemk  26763  pntlemo  26764  ostth2lem4  26793  ostth3  26795  tgbtwndiff  26876  tgifscgr  26878  trgcgrg  26885  motcgr3  26915  tgbtwnconn1lem1  26942  tgbtwnconn1lem2  26943  ismir  27029  miriso  27040  midexlem  27062  ragmir  27070  footexALT  27088  footexlem1  27089  footexlem2  27090  colperpexlem3  27102  mideulem2  27104  midex  27107  opphllem3  27119  midcgr  27150  lmiisolem  27166  brbtwn2  27282  colinearalglem4  27286  axsegconlem1  27294  axpaschlem  27317  axcontlem4  27344  axcontlem7  27347  axcontlem8  27348  ushgredgedgloop  27607  crctcshwlkn0lem6  28189  wwlknlsw  28221  wwlksnextwrd  28271  clwlkclwwlklem2a3  28367  clwlkclwwlk2  28376  clwwlkel  28419  clwwlkfo  28423  clwwlkext2edg  28429  eupth2eucrct  28590  numclwwlk2lem1lem  28715  numclwwlk1lem2fo  28731  numclwlk2lem2f  28750  grpoidinvlem2  28876  nvmtri  29042  cnnvm  29053  nvnd  29059  ipidsq  29081  ipnm  29082  ipipcj  29086  blocnilem  29175  ipasslem2  29203  dipsubdir  29219  hvaddsubval  29404  pjhthlem1  29762  pjspansn  29948  pjo  30042  unoplin  30291  adjadj  30307  hmoplin  30313  eigvec1  30333  lnopeqi  30379  nmcexi  30397  lnfnsubi  30417  riesz3i  30433  kbass6  30492  leoprf2  30498  leoprf  30499  pjnmopi  30519  mdslmd1lem1  30696  mdslmd1lem2  30697  superpos  30725  ifeq3da  30898  fgreu  31018  resf1o  31074  fprodex01  31148  wrdt2ind  31234  gsummpt2d  31318  xrge0tsmseq  31328  symgfcoeu  31360  psgnfzto1stlem  31376  psgnfzto1st  31381  cycpm2tr  31395  cycpmco2lem6  31407  cycpmco2lem7  31408  subrgchr  31500  rhmdvd  31529  nsgqusf1olem3  31609  ply1chr  31678  dimval  31695  dimvalfi  31696  lindsunlem  31714  dimkerim  31717  qusdimsum  31718  fedgmullem1  31719  extdg1id  31747  madjusmdetlem2  31787  qtophaus  31795  zarclssn  31832  zarcmplem  31840  pstmval  31854  mndpluscn  31885  qqhucn  31951  esumval  32023  gsumesum  32036  esumcst  32040  esumpcvgval  32055  oddpwdc  32330  eulerpartlemgvv  32352  probdif  32396  sgnmul  32518  signsvtn  32572  actfunsnf1o  32593  reprpmtf1o  32615  hgt750lemd  32637  logdivsqrle  32639  hgt750lemg  32643  hgt750lemb  32645  bnj1415  33027  swrdrevpfx  33087  pfxwlk  33094  derangen2  33145  subfaclefac  33147  subfaclim  33159  satom  33327  fmla  33352  mrsubrn  33484  sinccvglem  33639  bcprod  33713  filnetlem4  34579  curunc  35768  ltflcei  35774  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem24  35810  mblfinlem4  35826  ibladdnclem  35842  iblabsnc  35850  iblmulc2nc  35851  ftc1anclem6  35864  ftc1anclem8  35866  sdclem2  35909  ismtycnv  35969  heiborlem10  35987  lflvsass  37102  lkrscss  37119  eqlkr  37120  eqlkr3  37122  ldualvsdi2  37165  omllaw3  37266  cmtcomlemN  37269  cmtbr3N  37275  omlfh3N  37280  llnexchb2lem  37889  dalawlem7  37898  dalawlem11  37902  dalawlem12  37903  pol1N  37931  paddatclN  37970  4atexlemcnd  38093  ltrncoidN  38149  cdleme3b  38250  cdleme11  38291  cdleme15a  38295  cdleme22e  38365  cdleme22g  38369  cdlemg18b  38700  trlcoat  38744  cdlemk2  38853  cdlemk4  38855  cdlemki  38862  cdlemksv2  38868  cdlemk15  38876  cdlemk55a  38980  diainN  39078  dia2dimlem3  39087  dia2dimlem5  39089  dvhlveclem  39129  diaocN  39146  cdlemn4  39219  cdlemn8  39225  dihopelvalcpre  39269  dihmeetlem9N  39336  dih1dimatlem  39350  dihpN  39357  dochvalr3  39384  dochsat  39404  djhjlj  39424  dochdmm1  39431  dihjatcclem4  39442  dihjat1  39450  dihjat4  39454  dochsnkr2cl  39495  dochfl1  39497  lclkrlem2j  39537  mapdordlem2  39658  mapdrvallem2  39666  hdmap10  39861  lcmineqlem12  40055  3lexlogpow5ineq5  40075  aks4d1p1  40091  frlmvscadiccat  40244  frlmsnic  40270  fsuppind  40286  mhphf  40292  cnreeu  40445  flt4lem7  40503  negexpidd  40511  3cubeslem2  40514  3cubeslem3r  40516  mzpsubmpt  40572  irrapxlem3  40653  pellexlem6  40663  pell1234qrne0  40682  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell14qrdich  40698  pell1qrgaplem  40702  rmxluc  40765  rmyluc  40766  jm2.24nn  40788  jm2.18  40817  jm2.19lem2  40819  jm2.19lem3  40820  jm2.22  40824  jm2.23  40825  jm2.16nn0  40833  jm2.27c  40836  fnwe2lem2  40883  lmhmfgsplit  40918  hbtlem2  40956  reabssgn  41251  relexpmulnn  41324  relexpmulg  41325  ntrclsneine0lem  41681  int-addassocd  41792  dvconstbi  41959  bccm1k  41967  binomcxplemnotnn0  41981  fmptsnxp  42712  wessf1ornlem  42729  projf1o  42743  infnsuprnmpt  42803  lefldiveq  42838  lt4addmuld  42852  fzdifsuc2  42856  suplesup  42885  infrpge  42897  xrlexaddrp  42898  xralrple2  42900  infleinflem1  42916  supminfrnmpt  42992  supminfxr2  43016  fsumnncl  43120  limcperiod  43176  sumnnodd  43178  limcresiooub  43190  limcresioolb  43191  0ellimcdiv  43197  reclimc  43201  limsupval3  43240  limsupequzmpt2  43266  liminfval5  43313  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  liminfequzmpt2  43339  climliminflimsupd  43349  liminfltlem  43352  liminflbuz2  43363  sinmulcos  43413  coskpi2  43414  cncfdmsn  43438  cncfiooicclem1  43441  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  fperdvper  43467  dvnmptdivc  43486  dvnxpaek  43490  dvnmul  43491  dvnprodlem1  43494  dvnprodlem3  43496  itgcoscmulx  43517  itgsincmulx  43522  itgspltprt  43527  itgiccshift  43528  itgperiod  43529  sublevolico  43532  volioof  43535  ovolsplit  43536  fvvolioof  43537  fvvolicof  43539  stoweidlem22  43570  stoweidlem32  43580  wallispilem5  43617  stirlinglem5  43626  dirkertrigeqlem2  43647  dirkertrigeq  43649  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem13  43668  fourierdlem16  43671  fourierdlem19  43674  fourierdlem21  43676  fourierdlem22  43677  fourierdlem28  43683  fourierdlem32  43687  fourierdlem33  43688  fourierdlem42  43697  fourierdlem47  43701  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem56  43710  fourierdlem60  43714  fourierdlem61  43715  fourierdlem64  43718  fourierdlem66  43720  fourierdlem71  43725  fourierdlem73  43727  fourierdlem74  43728  fourierdlem76  43730  fourierdlem78  43732  fourierdlem79  43733  fourierdlem80  43734  fourierdlem81  43735  fourierdlem83  43737  fourierdlem88  43742  fourierdlem92  43746  fourierdlem93  43747  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem109  43763  fourierdlem111  43765  fouriersw  43779  elaa2lem  43781  etransclem24  43806  etransclem25  43807  etransclem35  43817  etransclem46  43828  rrndistlt  43838  rrxunitopnfi  43840  qndenserrnbl  43843  qndenserrnopnlem  43845  saldifcl2  43874  intsal  43876  sge0sn  43924  sge0ltfirp  43945  sge0iunmptlemre  43960  sge0fodjrnlem  43961  sge0isum  43972  sge0xaddlem1  43978  nnfoctbdjlem  44000  meassle  44008  ismeannd  44012  meadif  44024  meaiuninclem  44025  meaiininclem  44031  omeunile  44050  caragendifcl  44059  caratheodory  44073  isomenndlem  44075  ovnsubaddlem1  44115  hoidmv1lelem2  44137  hoidmv1le  44139  hoidmvlelem2  44141  hoidmvle  44145  hoi2toco  44152  rrnmbl  44159  hoidifhspdmvle  44165  voncmpl  44166  hoiqssbl  44170  hspmbllem1  44171  hspmbllem2  44172  ovolval2lem  44188  ovolval5lem2  44198  ovnovollem1  44201  ovnovollem2  44202  hoimbl2  44210  vonhoire  44217  salpreimagelt  44252  salpreimalegt  44254  preimaioomnf  44264  smfres  44335  smfmullem1  44336  smflimmpt  44354  smfsupmpt  44359  smfinfmpt  44363  smflimsupmpt  44373  smfliminflem  44374  smfliminfmpt  44376  sigarcol  44391  f1oresf1o  44793  elsprel  44938  prproropf1o  44970  paireqne  44974  sfprmdvdsmersenne  45066  lighneallem3  45070  lighneallem4  45073  nn0onn0exALTV  45162  nnsum3primesprm  45253  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  c0snmgmhm  45483  rngcifuestrc  45566  funcrngcsetc  45567  funcrngcsetcALT  45568  funcringcsetc  45604  funcringcsetcALTV2lem7  45611  funcringcsetclem7ALTV  45634  lincext3  45808  lincresunit3  45833  nn0onn0ex  45880  nnpw2pmod  45940  blennn0em1  45948  digexp  45964  dignn0ehalf  45974  nn0mulfsum  45981  itcovalpclem1  46027  eenglngeehlnmlem2  46095  rrx2vlinest  46098  line2  46109  itschlc0xyqsol  46124  itsclinecirc0b  46131  toplatjoin  46299  toplatmeet  46300  recsec  46469  reccsc  46470  aacllem  46516  amgmlemALT  46518
  Copyright terms: Public domain W3C validator