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

Theorem eqtr2d 2471
Description: An equality transitivity deduction. (Contributed by NM, 18-Oct-1999.)
Hypotheses
Ref Expression
eqtr2d.1  |-  ( ph  ->  A  =  B )
eqtr2d.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
eqtr2d  |-  ( ph  ->  C  =  A )

Proof of Theorem eqtr2d
StepHypRef Expression
1 eqtr2d.1 . . 3  |-  ( ph  ->  A  =  B )
2 eqtr2d.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2eqtrd 2470 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2437 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421
This theorem is referenced by:  3eqtrrd  2475  3eqtr2rd  2477  ifan  3961  ifor  3962  dfopif  4187  nvocnv  6195  elovmpt3rab1  6541  onsucmin  6662  csbopeq1a  6860  oaabs2  7354  ecinxp  7446  resixpfo  7568  sbthlem3  7690  rankxpsuc  8352  fseqenlem2  8454  dfac2  8559  isf32lem9  8789  compsscnvlem  8798  ttukeylem7  8943  fpwwe2lem11  9064  00id  9807  submul2  10058  mulsubfacd  10077  divadddiv  10321  infrenegsup  10591  infmsupOLD  10592  xadd4d  11589  fzdifsuc  11853  fzval3  11980  fzoshftral  12019  ceim1l  12071  fldiv  12084  flmod  12108  intfrac  12109  modcyc2  12130  moddi  12154  uzrdgfni  12169  axdc4uzlem  12192  seqf1olem1  12249  seqf1olem2  12250  seqid2  12256  expnegz  12303  binom2sub  12388  binom3  12390  wrdlenccats1lenm1  12741  ccatw2s1p2  12755  ccats1swrdeq  12810  swrdccatin12lem2  12830  swrdccatin12  12832  swrdccat3b  12837  cshweqrep  12905  2cshwcshw  12909  ccatco  12917  swrds2  12999  relexpsucnnr  13067  relexpaddnn  13093  reim  13151  mulre  13163  addcj  13190  absimle  13351  clim2ser  13696  isercoll2  13710  serf0  13725  iseralt  13729  summolem3  13758  isumclim3  13798  mptfzshft  13817  fsumrev  13818  fsum2mul  13828  incexc  13873  isumsplit  13876  mertenslem1  13918  fprodrev  14009  iprodclim3  14031  binomfallfaclem2  14071  ef4p  14145  tanval3  14166  efival  14184  sinmul  14204  bitsinvp1  14397  sadaddlem  14414  bitsshft  14423  smu01lem  14433  lcmgcdlem  14542  lcm1  14546  lcmfass  14590  eulerthlem2  14699  powm2modprm  14717  pythagtriplem16  14743  pczpre  14760  pcqdiv  14770  pcadd  14797  pcfac  14807  prmreclem5  14827  4sqlem10  14854  4sqlem19  14876  vdwapun  14887  vdwlem1  14894  ramcl  14950  strfvd  15117  strfv2d  15118  xpsff1o  15425  xpslem  15430  2oppccomf  15581  oppcepi  15595  sscfn1  15673  sscfn2  15674  invfuc  15830  funcestrcsetclem7  15982  funcsetcestrclem7  15997  grpinvssd  16682  grpinvval2  16688  pmtrdifwrdellem2  17074  psgnunilem1  17085  psgnuni  17091  pgp0  17183  sylow1lem1  17185  sylow3lem2  17215  efgredleme  17328  efgcpbllemb  17340  frgpuptinv  17356  frgpup3lem  17362  gexexlem  17425  cyggenod  17454  gsumval3eu  17473  gsumval3  17476  gsumzaddlem  17489  dprd2db  17611  ringinvdv  17857  lss1d  18121  pwssplit1  18217  mplcoe3  18625  subrgascl  18656  evlseu  18674  ply1sclid  18816  znzrh2  19047  regsumsupp  19121  ipassr2  19145  dsmmfi  19232  frlmlss  19245  frlmip  19267  frlmlbs  19286  frlmup3  19289  islindf4  19327  1marepvmarrepid  19531  madurid  19600  smadiadetlem3  19624  mat2pmatghm  19685  pmatcollpwscmatlem1  19744  pm2mpmhmlem2  19774  cpmadurid  19822  cpmidgsumm2pm  19824  cpmadugsumlemB  19829  cayhamlem2  19839  ntrval2  19997  ordtuni  20137  cnclima  20215  cmpsub  20346  ptbasfi  20527  txbasval  20552  pt1hmeo  20752  alexsubALTlem1  20993  trust  21175  ussid  21206  ressuss  21209  ressprdsds  21317  imasdsf1olem  21319  setsms  21426  tmsxms  21432  tmsxpsmopn  21483  subgnm  21572  tngnm  21590  tngngp2  21591  xrsxmet  21738  xrge0gsumle  21762  metdstri  21779  xrhmeo  21870  lebnumlem3  21887  pcorevlem  21950  pi1xfrcnvlem  21980  clmabs  22006  cvsmuleqdivd  22035  rrxip  22242  rrxds  22245  minveclem4a  22265  pjthlem1  22272  ovolunlem1a  22327  mbfres2  22478  i1faddlem  22528  ibladdlem  22654  iblabs  22663  ditgsplit  22693  dvnres  22762  dveflem  22808  dveq0  22829  dvfsumabs  22852  itgsubstlem  22877  ply1divex  22962  dgrco  23097  plycjlem  23098  taylthlem1  23193  pserdv2  23250  abelthlem6  23256  abelthlem7  23258  tangtx  23325  abssinper  23338  sineq0  23341  explog  23408  reexplog  23409  eflogeq  23416  abslogle  23432  tanarg  23433  logtayl  23470  logtayl2  23472  relogbdiv  23581  ang180lem3  23605  affineequiv  23617  affineequiv2  23618  chordthmlem4  23626  chordthmlem5  23627  heron  23629  dcubic1lem  23634  dcubic2  23635  dcubic  23637  mcubic  23638  cubic2  23639  dquartlem1  23642  dquart  23644  quart1lem  23646  quartlem1  23648  quart  23652  acoscos  23684  atanlogaddlem  23704  atantayl2  23729  atantayl3  23730  birthdaylem2  23743  efrlim  23760  amgmlem  23780  logdifbnd  23784  emcllem3  23788  emcllem6  23791  lgamgulmlem2  23820  lgamgulmlem3  23821  lgamgulmlem4  23822  lgamgulmlem5  23823  gamigam  23843  lgamcvg2  23845  gamfac  23857  basellem3  23872  basellem8  23877  basellem9  23878  chtprm  23943  logfaclbnd  24013  perfect1  24019  bcp1ctr  24070  bclbnd  24071  bposlem1  24075  lgsdilem  24113  lgsdirnn0  24130  lgsdinn0  24131  lgseisenlem2  24141  lgsquadlem1  24145  2sqlem2  24155  mul2sq  24156  vmadivsum  24183  rpvmasumlem  24188  dchrisumlem1  24190  dchrisumlem2  24191  dchrmusum2  24195  dchrvmasum2if  24198  dchrisum0lem2  24219  logsqvma2  24244  selberg3  24260  selberg4lem1  24261  pntrsumo1  24266  pntrlog2bndlem2  24279  pntrlog2bndlem3  24280  pntrlog2bndlem5  24282  pntibndlem2  24292  pntlemk  24307  pntlemo  24308  ostth2lem4  24337  ostth3  24339  tgbtwndiff  24413  tgifscgr  24416  trgcgrg  24422  motcgr3  24450  tgbtwnconn1lem1  24477  tgbtwnconn1lem2  24478  ismir  24564  miriso  24574  midexlem  24594  ragmir  24602  footex  24620  colperpexlem3  24631  mideulem2  24633  midex  24636  opphllem3  24648  midcgr  24678  lmiisolem  24694  brbtwn2  24781  colinearalglem4  24785  axsegconlem1  24793  axpaschlem  24816  axcontlem4  24843  axcontlem7  24846  axcontlem8  24847  wwlkextwrd  25301  clwwlkn2  25348  clwlkisclwwlklem2a3  25354  clwlkisclwwlk2  25363  clwwlkel  25366  clwwlkfo  25370  clwwlkext2edg  25375  wwlkext2clwwlk  25376  frg2woteq  25633  extwwlkfablem1  25647  clwwlkextfrlem1  25649  numclwlk1lem2foa  25664  numclwlk1lem2fo  25668  numclwlk2lem2f  25676  grpoidinvlem2  25778  gxid  25846  subgores  25877  nvmtri  26145  cnnvm  26159  nvnd  26165  ipidsq  26194  ipnm  26195  ipipcj  26199  blocnilem  26290  ipasslem2  26318  dipsubdir  26334  hvaddsubval  26521  pjhthlem1  26879  pjspansn  27065  pjo  27159  unoplin  27408  adjadj  27424  hmoplin  27430  eigvec1  27450  lnopeqi  27496  nmcexi  27514  lnfnsubi  27534  riesz3i  27550  kbass6  27609  leoprf2  27615  leoprf  27616  pjnmopi  27636  mdslmd1lem1  27813  mdslmd1lem2  27814  superpos  27842  fgreu  28114  resf1o  28158  2sqmod  28247  gsummpt2d  28382  xrge0tsmseq  28389  subrgchr  28396  rhmdvd  28423  symgfcoeu  28447  psgnfzto1stlem  28452  psgnfzto1st  28457  madjusmdetlem2  28493  qtophaus  28502  pstmval  28537  mndpluscn  28571  qqhucn  28635  esumval  28706  gsumesum  28719  esumcst  28723  esumpcvgval  28738  oddpwdc  29013  eulerpartlemgvv  29035  probdif  29079  ballotlemfp1  29150  sgnmul  29201  signsvtn  29261  bnj1415  29635  derangen2  29685  subfaclefac  29687  subfaclim  29699  mrsubrn  29939  sinccvglem  30104  bcprod  30161  filnetlem4  30822  ltflcei  31636  poimirlem16  31659  poimirlem17  31660  poimirlem19  31662  poimirlem20  31663  poimirlem24  31667  mblfinlem4  31683  ibladdnclem  31701  iblabsnc  31709  iblmulc2nc  31710  ftc1anclem6  31725  ftc1anclem8  31727  sdclem2  31774  ismtycnv  31837  heiborlem10  31855  lflvsass  32355  lkrscss  32372  eqlkr  32373  eqlkr3  32375  ldualvsdi2  32418  omllaw3  32519  cmtcomlemN  32522  cmtbr3N  32528  omlfh3N  32533  llnexchb2lem  33141  dalawlem7  33150  dalawlem11  33154  dalawlem12  33155  pol1N  33183  paddatclN  33222  4atexlemcnd  33345  ltrncoidN  33401  cdleme3b  33503  cdleme11  33544  cdleme15a  33548  cdleme22e  33619  cdleme22g  33623  cdlemg18b  33954  trlcoat  33998  cdlemk2  34107  cdlemk4  34109  cdlemki  34116  cdlemksv2  34122  cdlemk15  34130  cdlemk55a  34234  diainN  34333  dia2dimlem3  34342  dia2dimlem5  34344  dvhlveclem  34384  diaocN  34401  cdlemn4  34474  cdlemn8  34480  dihopelvalcpre  34524  dihmeetlem9N  34591  dih1dimatlem  34605  dihpN  34612  dochvalr3  34639  dochsat  34659  djhjlj  34679  dochdmm1  34686  dihjatcclem4  34697  dihjat1  34705  dihjat4  34709  dochsnkr2cl  34750  dochfl1  34752  lclkrlem2j  34792  mapdordlem2  34913  mapdrvallem2  34921  hdmap10  35119  mzpsubmpt  35293  irrapxlem3  35377  pellexlem6  35387  pell1234qrne0  35406  pell1234qrreccl  35407  pell1234qrmulcl  35408  pell14qrdich  35422  pell1qrgaplem  35426  rmxluc  35489  rmyluc  35490  jm2.24nn  35514  jm2.18  35548  jm2.19lem2  35550  jm2.19lem3  35551  jm2.22  35555  jm2.23  35556  jm2.16nn0  35564  jm2.27c  35567  fnwe2lem2  35614  lmhmfgsplit  35649  hbtlem2  35688  hashgcdeq  35773  relexpmulnn  35939  relexpmulg  35940  int-addassocd  36257  dvconstbi  36319  bccm1k  36327  binomcxplemnotnn0  36341  fmptsnxp  37053  wessf1ornlem  37081  founiiun0  37087  disjinfi  37090  lefldiveq  37114  lt4addmuld  37132  fzdifsuc2  37138  suplesup  37170  fsumnncl  37224  limcperiod  37279  sumnnodd  37281  limcresiooub  37294  limcresioolb  37295  0ellimcdiv  37301  reclimc  37305  sinmulcos  37311  coskpi2  37312  divcncf  37332  cncfdmsn  37339  cncfiooicclem1  37342  dvmptdiv  37360  fperdvper  37361  dvmptresicc  37362  dvnmptdivc  37381  dvnxpaek  37385  dvnmul  37386  dvnprodlem1  37389  dvnprodlem3  37391  itgcoscmulx  37414  itgsincmulx  37419  itgspltprt  37424  itgiccshift  37425  itgperiod  37426  stoweidlem22  37450  stoweidlem32  37461  wallispilem5  37499  stirlinglem5  37508  dirkertrigeqlem2  37529  dirkertrigeq  37531  dirkercncflem1  37533  dirkercncflem2  37534  dirkercncflem4  37536  fourierdlem13  37550  fourierdlem16  37553  fourierdlem19  37556  fourierdlem21  37558  fourierdlem22  37559  fourierdlem28  37565  fourierdlem32  37569  fourierdlem33  37570  fourierdlem42  37579  fourierdlem47  37584  fourierdlem48  37585  fourierdlem49  37586  fourierdlem50  37587  fourierdlem56  37593  fourierdlem60  37597  fourierdlem61  37598  fourierdlem64  37601  fourierdlem66  37603  fourierdlem71  37608  fourierdlem73  37610  fourierdlem74  37611  fourierdlem76  37613  fourierdlem78  37615  fourierdlem79  37616  fourierdlem80  37617  fourierdlem81  37618  fourierdlem83  37620  fourierdlem88  37625  fourierdlem92  37629  fourierdlem93  37630  fourierdlem97  37634  fourierdlem101  37638  fourierdlem103  37640  fourierdlem104  37641  fourierdlem109  37646  fourierdlem111  37648  fouriersw  37662  elaa2lem  37664  etransclem24  37689  etransclem25  37690  etransclem35  37700  etransclem46  37711  saldifcl2  37733  intsal  37735  sge0sn  37754  sge0ltfirp  37775  sge0iunmptlemre  37790  sge0fodjrnlem  37791  nnfoctbdjlem  37801  meassle  37809  ismeannd  37813  omeunile  37834  caragendifcl  37843  caratheodory  37857  sigarcol  37872  nn0onn0exALTV  38216  nnsum3primesprm  38274  nnsum4primesodd  38280  nnsum4primesoddALTV  38281  ccats1pfxeq  38351  pfxccatin12lem2  38354  pfxccatin12  38355  c0snmgmhm  38671  rngcifuestrc  38756  funcrngcsetc  38757  funcrngcsetcALT  38758  funcringcsetc  38794  funcringcsetcALTV2lem7  38801  funcringcsetclem7ALTV  38824  lincext3  39008  lincresunit3  39033  nn0onn0ex  39091  nnpw2pmod  39154  blennn0em1  39162  digexp  39178  dignn0ehalf  39188  nn0mulfsum  39195  recsec  39236  reccsc  39237  aacllem  39300
  Copyright terms: Public domain W3C validator