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

Theorem eqtr2d 2641
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 2640 . 2 (𝜑𝐴 = 𝐶)
43eqcomd 2612 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599
This theorem is referenced by:  3eqtrrd  2645  3eqtr2rd  2647  ifan  4080  ifor  4081  dfopif  4328  nvocnv  6412  elovmpt3rab1  6765  onsucmin  6887  csbopeq1a  7086  oaabs2  7586  ecinxp  7683  resixpfo  7806  sbthlem3  7931  rankxpsuc  8602  fseqenlem2  8705  dfac2  8810  isf32lem9  9040  compsscnvlem  9049  ttukeylem7  9194  fpwwe2lem11  9315  00id  10059  submul2  10318  mulsubfacd  10338  divadddiv  10586  infrenegsup  10850  xadd4d  11959  fzdifsuc  12222  fzval3  12356  fzoshftral  12399  ceim1l  12460  fldiv  12473  flmod  12498  intfrac  12499  modcyc2  12520  moddi  12552  uzrdgfni  12571  axdc4uzlem  12596  seqf1olem1  12654  seqf1olem2  12655  seqid2  12661  expnegz  12708  binom2sub  12795  binom3  12799  wrdlenccats1lenm1  13195  ccatw2s1p2  13209  ccats1swrdeq  13264  swrdccatin12lem2  13283  swrdccatin12  13285  swrdccat3b  13290  cshweqrep  13361  2cshwcshw  13365  ccatco  13375  swrds2  13476  relexpsucnnr  13556  relexpaddnn  13582  reim  13640  mulre  13652  addcj  13679  absimle  13840  clim2ser  14176  isercoll2  14190  serf0  14202  iseralt  14206  summolem3  14235  isumclim3  14275  mptfzshft  14295  fsumrev  14296  fsum2mul  14306  incexc  14351  isumsplit  14354  mertenslem1  14398  fprodrev  14489  iprodclim3  14513  binomfallfaclem2  14553  ef4p  14625  tanval3  14646  efival  14664  sinmul  14684  bitsinvp1  14952  sadaddlem  14969  bitsshft  14978  smu01lem  14988  dfgcd2  15044  lcmgcdlem  15100  lcm1  15104  lcmfass  15140  eulerthlem2  15268  hashgcdeq  15275  powm2modprm  15289  pythagtriplem16  15316  pczpre  15333  pcqdiv  15343  pcadd  15374  pcfac  15384  prmreclem5  15405  4sqlem10  15432  4sqlem19  15448  vdwapun  15459  vdwlem1  15466  ramcl  15514  strfvd  15675  strfv2d  15676  xpsff1o  15994  xpslem  15999  2oppccomf  16151  oppcepi  16165  sscfn1  16243  sscfn2  16244  invfuc  16400  funcestrcsetclem7  16552  funcsetcestrclem7  16567  grpinvssd  17258  grpinvval2  17264  pmtrdifwrdellem2  17668  psgnunilem1  17679  psgnuni  17685  pgp0  17777  sylow1lem1  17779  sylow3lem2  17809  efgredleme  17922  efgcpbllemb  17934  frgpuptinv  17950  frgpup3lem  17956  gexexlem  18021  cyggenod  18052  gsumval3eu  18071  gsumval3  18074  gsumzaddlem  18087  dprd2db  18208  ringinvdv  18460  lss1d  18727  pwssplit1  18823  mplcoe3  19230  subrgascl  19262  evlseu  19280  ply1sclid  19422  znzrh2  19655  regsumsupp  19729  ipassr2  19753  dsmmfi  19840  frlmlss  19853  frlmip  19875  frlmlbs  19894  frlmup3  19897  islindf4  19935  1marepvmarrepid  20139  madurid  20208  smadiadetlem3  20232  mat2pmatghm  20293  pmatcollpwscmatlem1  20352  pm2mpmhmlem2  20382  cpmadurid  20430  cpmidgsumm2pm  20432  cpmadugsumlemB  20437  cayhamlem2  20447  ntrval2  20604  ordtuni  20743  cnclima  20821  cmpsub  20952  ptbasfi  21133  txbasval  21158  pt1hmeo  21358  alexsubALTlem1  21600  trust  21782  ussid  21813  ressuss  21816  ressprdsds  21924  imasdsf1olem  21926  setsms  22033  tmsxms  22039  tmsxpsmopn  22090  subgnm  22182  tngnm  22200  tngngp2  22201  xrsxmet  22349  xrge0gsumle  22373  metdstri  22390  xrhmeo  22481  lebnumlem3  22498  pcorevlem  22562  pi1xfrcnvlem  22592  clmabs  22619  cvsmuleqdivd  22668  rrxip  22900  rrxds  22903  minveclem4a  22923  pjthlem1  22930  ovolunlem1a  22985  mbfres2  23132  i1faddlem  23180  ibladdlem  23306  iblabs  23315  ditgsplit  23345  dvnres  23414  dveflem  23460  dveq0  23481  dvfsumabs  23504  itgsubstlem  23529  ply1divex  23614  dgrco  23749  plycjlem  23750  taylthlem1  23845  pserdv2  23902  abelthlem6  23908  abelthlem7  23910  tangtx  23975  abssinper  23988  sineq0  23991  explog  24058  reexplog  24059  eflogeq  24066  abslogle  24082  tanarg  24083  logtayl  24120  logtayl2  24122  relogbdiv  24231  ang180lem3  24255  affineequiv  24267  affineequiv2  24268  chordthmlem4  24276  chordthmlem5  24277  heron  24279  dcubic1lem  24284  dcubic2  24285  dcubic  24287  mcubic  24288  cubic2  24289  dquartlem1  24292  dquart  24294  quart1lem  24296  quartlem1  24298  quart  24302  acoscos  24334  atanlogaddlem  24354  atantayl2  24379  atantayl3  24380  birthdaylem2  24393  efrlim  24410  amgmlem  24430  logdifbnd  24434  emcllem3  24438  emcllem6  24441  lgamgulmlem2  24470  lgamgulmlem3  24471  lgamgulmlem4  24472  lgamgulmlem5  24473  gamigam  24493  lgamcvg2  24495  gamfac  24507  basellem3  24523  basellem8  24528  basellem9  24529  chtprm  24593  logfaclbnd  24661  perfect1  24667  bcp1ctr  24718  bclbnd  24719  bposlem1  24723  lgsdilem  24763  lgsdirnn0  24783  lgsdinn0  24784  gausslemma2dlem1a  24804  gausslemma2dlem4  24808  gausslemma2dlem5a  24809  lgseisenlem2  24815  lgsquadlem1  24819  2sqlem2  24857  mul2sq  24858  vmadivsum  24885  rpvmasumlem  24890  dchrisumlem1  24892  dchrisumlem2  24893  dchrmusum2  24897  dchrvmasum2if  24900  dchrisum0lem2  24921  logsqvma2  24946  selberg3  24962  selberg4lem1  24963  pntrsumo1  24968  pntrlog2bndlem2  24981  pntrlog2bndlem3  24982  pntrlog2bndlem5  24984  pntibndlem2  24994  pntlemk  25009  pntlemo  25010  ostth2lem4  25039  ostth3  25041  tgbtwndiff  25115  tgifscgr  25118  trgcgrg  25125  motcgr3  25155  tgbtwnconn1lem1  25182  tgbtwnconn1lem2  25183  ismir  25269  miriso  25280  midexlem  25302  ragmir  25310  footex  25328  colperpexlem3  25339  mideulem2  25341  midex  25344  opphllem3  25356  midcgr  25387  lmiisolem  25403  brbtwn2  25500  colinearalglem4  25504  axsegconlem1  25512  axpaschlem  25535  axcontlem4  25562  axcontlem7  25565  axcontlem8  25566  wwlkextwrd  26019  clwwlkn2  26066  clwlkisclwwlklem2a3  26072  clwlkisclwwlk2  26081  clwwlkel  26084  clwwlkfo  26088  clwwlkext2edg  26093  wwlkext2clwwlk  26094  frg2woteq  26350  extwwlkfablem1  26364  clwwlkextfrlem1  26366  numclwlk1lem2foa  26381  numclwlk1lem2fo  26385  numclwlk2lem2f  26393  grpoidinvlem2  26506  nvmtri  26701  cnnvm  26715  nvnd  26721  ipidsq  26750  ipnm  26751  ipipcj  26755  blocnilem  26846  ipasslem2  26874  dipsubdir  26890  hvaddsubval  27077  pjhthlem1  27437  pjspansn  27623  pjo  27717  unoplin  27966  adjadj  27982  hmoplin  27988  eigvec1  28008  lnopeqi  28054  nmcexi  28072  lnfnsubi  28092  riesz3i  28108  kbass6  28167  leoprf2  28173  leoprf  28174  pjnmopi  28194  mdslmd1lem1  28371  mdslmd1lem2  28372  superpos  28400  fgreu  28657  resf1o  28696  2sqmod  28782  gsummpt2d  28915  xrge0tsmseq  28921  subrgchr  28928  rhmdvd  28955  symgfcoeu  28979  psgnfzto1stlem  28984  psgnfzto1st  28989  madjusmdetlem2  29025  qtophaus  29034  pstmval  29069  mndpluscn  29103  qqhucn  29167  esumval  29238  gsumesum  29251  esumcst  29255  esumpcvgval  29270  oddpwdc  29546  eulerpartlemgvv  29568  probdif  29612  sgnmul  29734  signsvtn  29790  bnj1415  30163  derangen2  30213  subfaclefac  30215  subfaclim  30227  mrsubrn  30467  sinccvglem  30623  bcprod  30680  filnetlem4  31349  curunc  32361  ltflcei  32367  matunitlindflem1  32375  matunitlindflem2  32376  poimirlem16  32395  poimirlem17  32396  poimirlem19  32398  poimirlem20  32399  poimirlem24  32403  mblfinlem4  32419  ibladdnclem  32436  iblabsnc  32444  iblmulc2nc  32445  ftc1anclem6  32460  ftc1anclem8  32462  sdclem2  32508  ismtycnv  32571  heiborlem10  32589  lflvsass  33186  lkrscss  33203  eqlkr  33204  eqlkr3  33206  ldualvsdi2  33249  omllaw3  33350  cmtcomlemN  33353  cmtbr3N  33359  omlfh3N  33364  llnexchb2lem  33972  dalawlem7  33981  dalawlem11  33985  dalawlem12  33986  pol1N  34014  paddatclN  34053  4atexlemcnd  34176  ltrncoidN  34232  cdleme3b  34334  cdleme11  34375  cdleme15a  34379  cdleme22e  34450  cdleme22g  34454  cdlemg18b  34785  trlcoat  34829  cdlemk2  34938  cdlemk4  34940  cdlemki  34947  cdlemksv2  34953  cdlemk15  34961  cdlemk55a  35065  diainN  35164  dia2dimlem3  35173  dia2dimlem5  35175  dvhlveclem  35215  diaocN  35232  cdlemn4  35305  cdlemn8  35311  dihopelvalcpre  35355  dihmeetlem9N  35422  dih1dimatlem  35436  dihpN  35443  dochvalr3  35470  dochsat  35490  djhjlj  35510  dochdmm1  35517  dihjatcclem4  35528  dihjat1  35536  dihjat4  35540  dochsnkr2cl  35581  dochfl1  35583  lclkrlem2j  35623  mapdordlem2  35744  mapdrvallem2  35752  hdmap10  35950  mzpsubmpt  36124  irrapxlem3  36206  pellexlem6  36216  pell1234qrne0  36235  pell1234qrreccl  36236  pell1234qrmulcl  36237  pell14qrdich  36251  pell1qrgaplem  36255  rmxluc  36319  rmyluc  36320  jm2.24nn  36344  jm2.18  36373  jm2.19lem2  36375  jm2.19lem3  36376  jm2.22  36380  jm2.23  36381  jm2.16nn0  36389  jm2.27c  36392  fnwe2lem2  36439  lmhmfgsplit  36474  hbtlem2  36513  relexpmulnn  36820  relexpmulg  36821  ntrclsneine0lem  37182  int-addassocd  37299  dvconstbi  37355  bccm1k  37363  binomcxplemnotnn0  37377  fmptsnxp  38143  wessf1ornlem  38166  founiiun0  38172  disjinfi  38175  projf1o  38181  lefldiveq  38246  lt4addmuld  38261  fzdifsuc2  38267  suplesup  38297  infrpge  38309  xrlexaddrp  38310  xralrple2  38312  infleinflem1  38328  fsumnncl  38439  limcperiod  38496  sumnnodd  38498  limcresiooub  38510  limcresioolb  38511  0ellimcdiv  38517  reclimc  38521  sinmulcos  38549  coskpi2  38550  divcncf  38570  cncfdmsn  38577  cncfiooicclem1  38580  fprodsubrecnncnvlem  38595  fprodaddrecnncnvlem  38597  dvmptdiv  38608  fperdvper  38609  dvmptresicc  38610  dvnmptdivc  38629  dvnxpaek  38633  dvnmul  38634  dvnprodlem1  38637  dvnprodlem3  38639  itgcoscmulx  38662  itgsincmulx  38667  itgspltprt  38672  itgiccshift  38673  itgperiod  38674  sublevolico  38678  volioof  38681  ovolsplit  38682  fvvolioof  38683  fvvolicof  38685  stoweidlem22  38716  stoweidlem32  38726  wallispilem5  38763  stirlinglem5  38772  dirkertrigeqlem2  38793  dirkertrigeq  38795  dirkercncflem1  38797  dirkercncflem2  38798  dirkercncflem4  38800  fourierdlem13  38814  fourierdlem16  38817  fourierdlem19  38820  fourierdlem21  38822  fourierdlem22  38823  fourierdlem28  38829  fourierdlem32  38833  fourierdlem33  38834  fourierdlem42  38843  fourierdlem47  38847  fourierdlem48  38848  fourierdlem49  38849  fourierdlem50  38850  fourierdlem56  38856  fourierdlem60  38860  fourierdlem61  38861  fourierdlem64  38864  fourierdlem66  38866  fourierdlem71  38871  fourierdlem73  38873  fourierdlem74  38874  fourierdlem76  38876  fourierdlem78  38878  fourierdlem79  38879  fourierdlem80  38880  fourierdlem81  38881  fourierdlem83  38883  fourierdlem88  38888  fourierdlem92  38892  fourierdlem93  38893  fourierdlem97  38897  fourierdlem101  38901  fourierdlem103  38903  fourierdlem104  38904  fourierdlem109  38909  fourierdlem111  38911  fouriersw  38925  elaa2lem  38927  etransclem24  38952  etransclem25  38953  etransclem35  38963  etransclem46  38974  rrxdsfi  38982  rrndistlt  38987  rrxunitopnfi  38989  qndenserrnbl  38992  qndenserrnopnlem  38994  saldifcl2  39023  intsal  39025  sge0sn  39073  sge0ltfirp  39094  sge0iunmptlemre  39109  sge0fodjrnlem  39110  sge0isum  39121  sge0xaddlem1  39127  nnfoctbdjlem  39149  meassle  39157  ismeannd  39161  meadif  39173  meaiuninclem  39174  meaiininclem  39177  omeunile  39196  caragendifcl  39205  caratheodory  39219  isomenndlem  39221  ovnsubaddlem1  39261  hoidmv1lelem2  39283  hoidmv1le  39285  hoidmvlelem2  39287  hoidmvle  39291  hoi2toco  39298  rrnmbl  39305  hoidifhspdmvle  39311  voncmpl  39312  hoiqssbl  39316  hspmbllem1  39317  hspmbllem2  39318  ovolval2lem  39334  ovolval5lem2  39344  ovnovollem1  39347  ovnovollem2  39348  hoimbl2  39356  vonhoire  39364  salpreimagelt  39396  salpreimalegt  39398  preimaioomnf  39407  smfres  39476  smfmullem1  39477  sigarcol  39503  sfprmdvdsmersenne  39860  lighneallem3  39864  lighneallem4  39867  nn0onn0exALTV  39949  nnsum3primesprm  40008  nnsum4primesodd  40014  nnsum4primesoddALTV  40015  ccats1pfxeq  40086  pfxccatin12lem2  40089  pfxccatin12  40090  ushgredgedgaloop  40457  crctcsh1wlkn0lem6  41017  wwlksnextwrd  41102  clwlkclwwlklem2a3  41202  clwlkclwwlk2  41211  clwwlksel  41220  clwwlksfo  41224  clwwlksext2edg  41229  wwlksext2clwwlk  41230  eupth2eucrct  41384  av-clwwlkextfrlem1  41508  av-numclwlk1lem2foa  41520  av-numclwlk1lem2fo  41524  av-numclwlk2lem2f  41532  c0snmgmhm  41703  rngcifuestrc  41788  funcrngcsetc  41789  funcrngcsetcALT  41790  funcringcsetc  41826  funcringcsetcALTV2lem7  41833  funcringcsetclem7ALTV  41856  lincext3  42038  lincresunit3  42063  nn0onn0ex  42111  nnpw2pmod  42174  blennn0em1  42182  digexp  42198  dignn0ehalf  42208  nn0mulfsum  42215  recsec  42256  reccsc  42257  aacllem  42316  amgmlemALT  42318
  Copyright terms: Public domain W3C validator