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

Theorem eqtr2d 2860
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 2859 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2830 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817
This theorem is referenced by:  3eqtrrd  2864  3eqtr2rd  2866  ifan  4500  ifor  4501  dfopif  4784  nvocnv  7027  elovmpt3rab1  7395  onsucmin  7526  csbopeq1a  7739  oaabs2  8262  ecinxp  8362  resixpfo  8490  sbthlem3  8620  rankxpsuc  9302  fseqenlem2  9443  dfac2b  9548  isf32lem9  9775  compsscnvlem  9784  ttukeylem7  9929  fpwwe2lem11  10054  00id  10807  submul2  11072  mulsubfacd  11093  divadddiv  11347  infrenegsup  11616  xadd4d  12689  fzdifsuc  12967  fzval3  13106  fzoshftral  13154  ceim1l  13215  fldiv  13228  flmod  13253  intfrac  13254  modcyc2  13275  moddi  13307  uzrdgfni  13326  axdc4uzlem  13351  seqf1olem1  13410  seqf1olem2  13411  seqid2  13417  expnegz  13464  binom2sub  13582  binom3  13586  hashreshashfun  13801  ccatw2s1p2  13993  ccats1pfxeq  14072  pfxccatin12lem2  14089  pfxccatin12  14091  swrdccat3b  14098  cshweqrep  14179  2cshwcshw  14183  ccatco  14193  swrds2  14298  relexpsucnnr  14380  relexpaddnn  14406  reim  14464  mulre  14476  addcj  14503  absimle  14665  clim2ser  15007  isercoll2  15021  serf0  15033  iseralt  15037  summolem3  15067  isumclim3  15110  mptfzshft  15129  fsumrev  15130  fsum2mul  15140  incexc  15188  isumsplit  15191  mertenslem1  15236  fprodrev  15327  iprodclim3  15350  binomfallfaclem2  15390  ef4p  15462  tanval3  15483  efival  15501  sinmul  15521  bitsinvp1  15792  sadaddlem  15809  bitsshft  15818  smu01lem  15828  dfgcd2  15888  lcmgcdlem  15944  lcm1  15948  lcmfass  15984  eulerthlem2  16113  hashgcdeq  16120  powm2modprm  16134  pythagtriplem16  16161  pczpre  16178  pcqdiv  16188  pcadd  16219  pcfac  16229  prmreclem5  16250  4sqlem10  16277  4sqlem19  16293  vdwapun  16304  vdwlem1  16311  ramcl  16359  setsstruct  16519  strfvd  16524  strfv2d  16525  xpsff1o  16836  xpsrnbas  16840  2oppccomf  16991  oppcepi  17005  sscfn1  17083  sscfn2  17084  invfuc  17240  funcestrcsetclem7  17392  funcsetcestrclem7  17407  gsumsplit1r  17893  grpinvssd  18172  grpinvval2  18178  cycsubggend  18344  pmtrdifwrdellem2  18606  psgnunilem1  18617  psgnuni  18623  pgp0  18717  sylow1lem1  18719  sylow3lem2  18749  efgredleme  18865  efgcpbllemb  18877  frgpuptinv  18893  frgpup3lem  18899  gexexlem  18968  cyggenod  18999  gsumval3eu  19020  gsumval3  19023  gsumzaddlem  19037  dprd2db  19161  ablsimpgfindlem1  19225  ringinvdv  19440  lss1d  19728  pwssplit1  19824  mplcoe3  20240  subrgascl  20271  evlseu  20289  mhpinvcl  20332  ply1sclid  20449  znzrh2  20685  regsumsupp  20759  ipassr2  20784  dsmmfi  20875  frlmlss  20888  frlmip  20915  frlmlbs  20934  frlmup3  20937  islindf4  20975  1marepvmarrepid  21177  madurid  21246  smadiadetlem3  21270  mat2pmatghm  21331  pmatcollpwscmatlem1  21390  pm2mpmhmlem2  21420  cpmadurid  21468  cpmidgsumm2pm  21470  cpmadugsumlemB  21475  cayhamlem2  21485  ntrval2  21652  ordtuni  21791  cnclima  21869  cmpsub  22001  ptbasfi  22182  txbasval  22207  pt1hmeo  22407  alexsubALTlem1  22648  trust  22831  ussid  22862  ressuss  22865  ressprdsds  22974  imasdsf1olem  22976  setsms  23083  tmsxms  23089  tmsxpsmopn  23140  subgnm  23235  tngnm  23253  tngngp2  23254  xrsxmet  23410  xrge0gsumle  23434  metdstri  23452  xrhmeo  23547  lebnumlem3  23564  pcorevlem  23627  pi1xfrcnvlem  23657  clmabs  23684  cvsmuleqdivd  23735  rrxip  23990  rrxds  23993  rrxdsfi  24011  minveclem4a  24030  pjthlem1  24037  divcncf  24047  ovolunlem1a  24096  mbfres2  24245  i1faddlem  24293  ibladdlem  24419  iblabs  24428  ditgsplit  24460  dvmptresicc  24515  dvnres  24530  dvmptdiv  24573  dveflem  24578  dveq0  24599  dvfsumabs  24622  itgsubstlem  24647  ply1divex  24733  dgrco  24868  plycjlem  24869  taylthlem1  24964  pserdv2  25021  abelthlem6  25027  abelthlem7  25029  tangtx  25094  abssinper  25109  sineq0  25112  explog  25181  reexplog  25182  eflogeq  25189  abslogle  25205  tanarg  25206  logtayl  25247  logtayl2  25249  relogbdiv  25361  ang180lem3  25393  affineequiv  25405  affineequiv2  25406  chordthmlem4  25417  chordthmlem5  25418  heron  25420  dcubic1lem  25425  dcubic2  25426  dcubic  25428  mcubic  25429  cubic2  25430  dquartlem1  25433  dquart  25435  quart1lem  25437  quartlem1  25439  quart  25443  acoscos  25475  atanlogaddlem  25495  atantayl2  25520  atantayl3  25521  birthdaylem2  25534  efrlim  25551  amgmlem  25571  logdifbnd  25575  emcllem3  25579  emcllem6  25582  lgamgulmlem2  25611  lgamgulmlem3  25612  lgamgulmlem4  25613  lgamgulmlem5  25614  gamigam  25634  lgamcvg2  25636  gamfac  25648  basellem3  25664  basellem8  25669  basellem9  25670  chtprm  25734  logfaclbnd  25802  perfect1  25808  bcp1ctr  25859  bclbnd  25860  bposlem1  25864  lgsdilem  25904  lgsdirnn0  25924  lgsdinn0  25925  gausslemma2dlem1a  25945  gausslemma2dlem4  25949  gausslemma2dlem5a  25950  lgseisenlem2  25956  lgsquadlem1  25960  2sqlem2  25998  mul2sq  25999  2sqmod  26016  2sqnn0  26018  vmadivsum  26062  rpvmasumlem  26067  dchrisumlem1  26069  dchrisumlem2  26070  dchrmusum2  26074  dchrvmasum2if  26077  dchrisum0lem2  26098  logsqvma2  26123  selberg3  26139  selberg4lem1  26140  pntrsumo1  26145  pntrlog2bndlem2  26158  pntrlog2bndlem3  26159  pntrlog2bndlem5  26161  pntibndlem2  26171  pntlemk  26186  pntlemo  26187  ostth2lem4  26216  ostth3  26218  tgbtwndiff  26296  tgifscgr  26298  trgcgrg  26305  motcgr3  26335  tgbtwnconn1lem1  26362  tgbtwnconn1lem2  26363  ismir  26449  miriso  26460  midexlem  26482  ragmir  26490  footexALT  26508  footexlem1  26509  footexlem2  26510  colperpexlem3  26522  mideulem2  26524  midex  26527  opphllem3  26539  midcgr  26570  lmiisolem  26586  brbtwn2  26695  colinearalglem4  26699  axsegconlem1  26707  axpaschlem  26730  axcontlem4  26757  axcontlem7  26760  axcontlem8  26761  ushgredgedgloop  27017  crctcshwlkn0lem6  27597  wwlknlsw  27629  wwlksnextwrd  27679  clwlkclwwlklem2a3  27775  clwlkclwwlk2  27784  clwwlkel  27827  clwwlkfo  27831  clwwlkext2edg  27837  eupth2eucrct  27998  numclwwlk2lem1lem  28123  numclwwlk1lem2fo  28139  numclwlk2lem2f  28158  grpoidinvlem2  28284  nvmtri  28450  cnnvm  28461  nvnd  28467  ipidsq  28489  ipnm  28490  ipipcj  28494  blocnilem  28583  ipasslem2  28611  dipsubdir  28627  hvaddsubval  28812  pjhthlem1  29170  pjspansn  29356  pjo  29450  unoplin  29699  adjadj  29715  hmoplin  29721  eigvec1  29741  lnopeqi  29787  nmcexi  29805  lnfnsubi  29825  riesz3i  29841  kbass6  29900  leoprf2  29906  leoprf  29907  pjnmopi  29927  mdslmd1lem1  30104  mdslmd1lem2  30105  superpos  30133  ifeq3da  30305  fgreu  30421  resf1o  30470  fprodex01  30545  wrdt2ind  30631  gsummpt2d  30712  xrge0tsmseq  30719  symgfcoeu  30751  psgnfzto1stlem  30767  psgnfzto1st  30772  cycpm2tr  30786  cycpmco2lem6  30798  cycpmco2lem7  30799  subrgchr  30890  rhmdvd  30919  dimval  31029  dimvalfi  31030  lindsunlem  31048  dimkerim  31051  qusdimsum  31052  fedgmullem1  31053  fedgmullem2  31054  extdg1id  31081  madjusmdetlem2  31121  qtophaus  31128  pstmval  31163  mndpluscn  31194  qqhucn  31258  esumval  31330  gsumesum  31343  esumcst  31347  esumpcvgval  31362  oddpwdc  31637  eulerpartlemgvv  31659  probdif  31703  sgnmul  31825  signsvtn  31879  actfunsnf1o  31900  reprpmtf1o  31922  hgt750lemd  31944  logdivsqrle  31946  hgt750lemg  31950  hgt750lemb  31952  bnj1415  32335  swrdrevpfx  32388  pfxwlk  32395  derangen2  32446  subfaclefac  32448  subfaclim  32460  satom  32628  fmla  32653  mrsubrn  32785  sinccvglem  32940  bcprod  32995  filnetlem4  33754  curunc  34949  ltflcei  34955  matunitlindflem1  34963  matunitlindflem2  34964  poimirlem16  34983  poimirlem17  34984  poimirlem19  34986  poimirlem20  34987  poimirlem24  34991  mblfinlem4  35007  ibladdnclem  35023  iblabsnc  35031  iblmulc2nc  35032  ftc1anclem6  35045  ftc1anclem8  35047  sdclem2  35090  ismtycnv  35150  heiborlem10  35168  lflvsass  36287  lkrscss  36304  eqlkr  36305  eqlkr3  36307  ldualvsdi2  36350  omllaw3  36451  cmtcomlemN  36454  cmtbr3N  36460  omlfh3N  36465  llnexchb2lem  37074  dalawlem7  37083  dalawlem11  37087  dalawlem12  37088  pol1N  37116  paddatclN  37155  4atexlemcnd  37278  ltrncoidN  37334  cdleme3b  37435  cdleme11  37476  cdleme15a  37480  cdleme22e  37550  cdleme22g  37554  cdlemg18b  37885  trlcoat  37929  cdlemk2  38038  cdlemk4  38040  cdlemki  38047  cdlemksv2  38053  cdlemk15  38061  cdlemk55a  38165  diainN  38263  dia2dimlem3  38272  dia2dimlem5  38274  dvhlveclem  38314  diaocN  38331  cdlemn4  38404  cdlemn8  38410  dihopelvalcpre  38454  dihmeetlem9N  38521  dih1dimatlem  38535  dihpN  38542  dochvalr3  38569  dochsat  38589  djhjlj  38609  dochdmm1  38616  dihjatcclem4  38627  dihjat1  38635  dihjat4  38639  dochsnkr2cl  38680  dochfl1  38682  lclkrlem2j  38722  mapdordlem2  38843  mapdrvallem2  38851  hdmap10  39046  lcmineqlem12  39234  frlmvscadiccat  39317  frlmsnic  39329  negexpidd  39476  3cubeslem2  39479  3cubeslem3r  39481  mzpsubmpt  39537  irrapxlem3  39618  pellexlem6  39628  pell1234qrne0  39647  pell1234qrreccl  39648  pell1234qrmulcl  39649  pell14qrdich  39663  pell1qrgaplem  39667  rmxluc  39730  rmyluc  39731  jm2.24nn  39753  jm2.18  39782  jm2.19lem2  39784  jm2.19lem3  39785  jm2.22  39789  jm2.23  39790  jm2.16nn0  39798  jm2.27c  39801  fnwe2lem2  39848  lmhmfgsplit  39883  hbtlem2  39921  reabssgn  40189  relexpmulnn  40263  relexpmulg  40264  ntrclsneine0lem  40623  int-addassocd  40736  dvconstbi  40895  bccm1k  40903  binomcxplemnotnn0  40917  fmptsnxp  41653  wessf1ornlem  41673  projf1o  41687  infnsuprnmpt  41750  lefldiveq  41787  lt4addmuld  41801  fzdifsuc2  41805  suplesup  41834  infrpge  41846  xrlexaddrp  41847  xralrple2  41849  infleinflem1  41865  supminfrnmpt  41945  supminfxr2  41971  fsumnncl  42076  limcperiod  42133  sumnnodd  42135  limcresiooub  42147  limcresioolb  42148  0ellimcdiv  42154  reclimc  42158  limsupval3  42197  limsupequzmpt2  42223  liminfval5  42270  limsupresxr  42271  liminfresxr  42272  liminfvalxr  42288  liminfequzmpt2  42296  climliminflimsupd  42306  liminfltlem  42309  liminflbuz2  42320  sinmulcos  42370  coskpi2  42371  cncfdmsn  42395  cncfiooicclem1  42398  fprodsubrecnncnvlem  42412  fprodaddrecnncnvlem  42414  fperdvper  42424  dvnmptdivc  42443  dvnxpaek  42447  dvnmul  42448  dvnprodlem1  42451  dvnprodlem3  42453  itgcoscmulx  42474  itgsincmulx  42479  itgspltprt  42484  itgiccshift  42485  itgperiod  42486  sublevolico  42489  volioof  42492  ovolsplit  42493  fvvolioof  42494  fvvolicof  42496  stoweidlem22  42527  stoweidlem32  42537  wallispilem5  42574  stirlinglem5  42583  dirkertrigeqlem2  42604  dirkertrigeq  42606  dirkercncflem1  42608  dirkercncflem2  42609  dirkercncflem4  42611  fourierdlem13  42625  fourierdlem16  42628  fourierdlem19  42631  fourierdlem21  42633  fourierdlem22  42634  fourierdlem28  42640  fourierdlem32  42644  fourierdlem33  42645  fourierdlem42  42654  fourierdlem47  42658  fourierdlem48  42659  fourierdlem49  42660  fourierdlem50  42661  fourierdlem56  42667  fourierdlem60  42671  fourierdlem61  42672  fourierdlem64  42675  fourierdlem66  42677  fourierdlem71  42682  fourierdlem73  42684  fourierdlem74  42685  fourierdlem76  42687  fourierdlem78  42689  fourierdlem79  42690  fourierdlem80  42691  fourierdlem81  42692  fourierdlem83  42694  fourierdlem88  42699  fourierdlem92  42703  fourierdlem93  42704  fourierdlem97  42708  fourierdlem101  42712  fourierdlem103  42714  fourierdlem104  42715  fourierdlem109  42720  fourierdlem111  42722  fouriersw  42736  elaa2lem  42738  etransclem24  42763  etransclem25  42764  etransclem35  42774  etransclem46  42785  rrndistlt  42795  rrxunitopnfi  42797  qndenserrnbl  42800  qndenserrnopnlem  42802  saldifcl2  42831  intsal  42833  sge0sn  42881  sge0ltfirp  42902  sge0iunmptlemre  42917  sge0fodjrnlem  42918  sge0isum  42929  sge0xaddlem1  42935  nnfoctbdjlem  42957  meassle  42965  ismeannd  42969  meadif  42981  meaiuninclem  42982  meaiininclem  42988  omeunile  43007  caragendifcl  43016  caratheodory  43030  isomenndlem  43032  ovnsubaddlem1  43072  hoidmv1lelem2  43094  hoidmv1le  43096  hoidmvlelem2  43098  hoidmvle  43102  hoi2toco  43109  rrnmbl  43116  hoidifhspdmvle  43122  voncmpl  43123  hoiqssbl  43127  hspmbllem1  43128  hspmbllem2  43129  ovolval2lem  43145  ovolval5lem2  43155  ovnovollem1  43158  ovnovollem2  43159  hoimbl2  43167  vonhoire  43174  salpreimagelt  43206  salpreimalegt  43208  preimaioomnf  43217  smfres  43285  smfmullem1  43286  smflimmpt  43304  smfsupmpt  43309  smfinfmpt  43313  smflimsupmpt  43323  smfliminflem  43324  smfliminfmpt  43326  sigarcol  43341  f1oresf1o  43709  elsprel  43855  prproropf1o  43887  paireqne  43891  sfprmdvdsmersenne  43984  lighneallem3  43988  lighneallem4  43991  nn0onn0exALTV  44080  nnsum3primesprm  44171  nnsum4primesodd  44177  nnsum4primesoddALTV  44178  c0snmgmhm  44401  rngcifuestrc  44484  funcrngcsetc  44485  funcrngcsetcALT  44486  funcringcsetc  44522  funcringcsetcALTV2lem7  44529  funcringcsetclem7ALTV  44552  lincext3  44727  lincresunit3  44752  nn0onn0ex  44799  nnpw2pmod  44859  blennn0em1  44867  digexp  44883  dignn0ehalf  44893  nn0mulfsum  44900  itcovalpclem1  44935  eenglngeehlnmlem2  45003  rrx2vlinest  45006  line2  45017  itschlc0xyqsol  45032  itsclinecirc0b  45039  recsec  45133  reccsc  45134  aacllem  45180  amgmlemALT  45182
  Copyright terms: Public domain W3C validator