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

Theorem syl6eqr 2335
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6eqr.1  |-  ( ph  ->  A  =  B )
syl6eqr.2  |-  C  =  B
Assertion
Ref Expression
syl6eqr  |-  ( ph  ->  A  =  C )

Proof of Theorem syl6eqr
StepHypRef Expression
1 syl6eqr.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6eqr.2 . . 3  |-  C  =  B
32eqcomi 2289 . 2  |-  B  =  C
41, 3syl6eq 2333 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625
This theorem is referenced by:  3eqtr4g  2342  iinrab2  3967  relop  4836  dfiun3g  4933  dfiin3g  4934  resima2  4990  relcnvfld  5205  uniabio  5231  iotanul  5236  dffn5  5570  dfimafn2  5574  fncnvima2  5649  fmptcof  5694  fcoconst  5697  resfunexg  5739  ffnov  5950  fnov  5954  fnrnov  5995  foov  5996  funimassov  5999  ovelimab  6000  ofc12  6104  caofinvl  6106  1st2val  6147  2nd2val  6148  curry1  6212  curry2  6215  dftpos3  6254  riotav  6311  riotauni  6313  tz7.44-3  6423  rdgsucmptnf  6444  rdglim2a  6448  frsucmptn  6453  seqomlem1  6464  seqomlem4  6467  oa0r  6539  om1r  6543  oarec  6562  oacomf1olem  6564  oeeulem  6601  omabs  6647  ecinxp  6736  mapunen  7032  phplem1  7042  fodomfi  7137  iinfi  7173  fiin  7177  dffi3  7186  ordtypelem3  7237  ordtypelem9  7243  cantnffval  7366  cantnfval  7371  cantnfp1lem3  7384  cantnflem1  7393  wemapwe  7402  oef1o  7403  cnfcom2lem  7406  rankuni  7537  cardval2  7626  dfac8alem  7658  dfac12lem1  7771  cda1dif  7804  cdaassen  7810  isf34lem4  8005  hsmexlem5  8058  axdc3lem4  8081  axdc4lem  8083  ac6num  8108  zorn2lem1  8125  ttukeylem3  8140  pwcfsdom  8207  fpwwe2lem9  8262  canth4  8271  canthp1lem2  8277  genpass  8635  prlem934  8659  mulcmpblnrlem  8697  recexsrlem  8727  supsrlem  8735  axrnegex  8786  nneo  10097  cnref1o  10351  xmulneg1  10591  xmulpnf1n  10600  xadddi  10617  fztp  10843  fseq1m1p1  10860  uzrdgsuci  11025  mulexpz  11144  expaddz  11148  bcp1m1  11334  seqcoll  11403  iswrdi  11419  cjexp  11637  rexuz3  11834  limsupval  11950  limsupgle  11953  climconst  12019  zsum  12193  fsum  12195  sum0  12196  sumz  12197  fsumcnv  12238  incexc2  12299  mertenslem2  12343  efval2  12367  ege2le3  12373  efzval  12384  efival  12434  sinbnd  12462  cosbnd  12463  sadfval  12645  bitsres  12666  smufval  12670  smupp1  12673  eucalgval  12754  eucalginv  12756  eucalglt  12757  eucalgcvga  12758  eucalg  12759  dfphi2  12844  phimullem  12849  prmdiv  12855  odzval  12858  pcval  12899  pczpre  12902  pcrec  12913  prmreclem6  12970  4sqlem17  13010  vdwmc  13027  vdwpc  13029  vdwlem8  13037  ramval  13057  ramcl  13078  ressval  13197  resslem  13203  firest  13339  topnval  13341  prdsval  13357  prdsleval  13378  prdsbas3  13382  prdsdsval2  13385  pwsval  13387  pwsbas  13388  pwselbasb  13389  pwsplusgval  13391  pwsmulrval  13392  pwsle  13393  pwsvscafval  13395  imasval  13416  imasdsval  13420  imasdsval2  13421  divsval  13446  xpsval  13476  xpslem  13477  xpsaddlem  13479  xpsvsca  13483  xpsle  13485  mrisval  13534  iscat  13576  cidfval  13580  homffval  13596  comfffval  13603  comffval  13604  comfeq  13611  oppcval  13618  oppchomfval  13619  oppccofval  13621  oppcbas  13623  oppcid  13626  monfval  13637  oppcmon  13643  sectffval  13655  invffval  13662  isoval  13669  isssc  13699  rescbas  13708  reschomf  13710  issubc  13714  isfunc  13740  isfuncd  13741  funcf2  13744  idfuval  13752  idfu2nd  13753  cofucl  13764  resfval2  13769  resf2nd  13771  funcres2b  13773  funcpropd  13776  isfull  13786  isfth  13790  natfval  13822  fucval  13834  fuccofval  13835  fucbas  13836  fuchom  13837  homafval  13863  homaval  13865  homadmcd  13876  arwval  13877  arwhoma  13879  idafval  13891  coafval  13898  coapm  13905  catcco  13935  catcid  13937  catcisolem  13940  xpcval  13953  xpcco  13959  1stfval  13967  2ndfval  13970  xpcpropd  13984  evlfval  13993  evlfcllem  13997  evlfcl  13998  curfval  13999  curf1cl  14004  curfcl  14008  uncf1  14012  uncf2  14013  uncfcurf  14015  diag2  14021  curf2ndf  14023  hofval  14028  hof2fval  14031  hofcl  14035  yonval  14037  hofpropd  14043  yonedalem21  14049  yonedalem22  14054  yonedalem3  14056  yonedainv  14057  yonffthlem  14058  isdrs  14070  ispos  14083  pltfval  14095  lubfval  14114  glbfval  14119  joinfval  14123  meetfval  14130  p0val  14149  p1val  14150  islat  14155  isclat  14217  ipoval  14259  isipodrs  14266  isdlat  14298  istsr  14328  spwval2  14335  isla  14344  isdir  14356  ismnd  14371  plusffval  14381  grpidval  14386  ismgmid  14389  pws0g  14410  ismhm  14419  submacs  14444  gsumvalx  14453  frmdval  14475  isgrp  14495  grpn0  14516  grpinvfval  14522  grpsubfval  14526  mulgfval  14570  mulgval  14571  mulgnn0p1  14580  pwsinvg  14609  issubg  14623  isnsg  14648  eqgfval  14667  divseccl  14675  isghm  14685  conjsubg  14716  conjsubgen  14717  isgim  14728  isga  14747  symgval  14773  cntrval  14797  cntzfval  14798  oppgval  14822  invoppggim  14835  odfval  14850  odval  14851  gexval  14891  ispgp  14905  sylow1lem1  14911  slwispgp  14924  pgpssslw  14927  sylow2alem2  14931  sylow3lem5  14944  lsmfval  14951  pj1fval  15005  efgmnvl  15025  efgval  15028  efgval2  15035  efginvrel2  15038  efgsfo  15050  efgredleme  15054  efgredlemd  15055  efgredlemc  15056  frgpval  15069  frgpeccl  15072  vrgpfval  15077  frgpuptinv  15082  frgpup3lem  15088  iscmn  15098  subcmn  15135  frgpnabllem1  15163  iscyg  15168  lt6abl  15183  gsumval3  15193  gsumzf1o  15198  gsum2d  15225  gsumcom2  15228  dmdprd  15238  dprdval  15240  dprd2da  15279  dmdprdsplit2lem  15282  dpjfval  15292  pgpfaclem1  15318  mgpval  15330  mgpplusg  15331  isrng  15347  iscrng  15350  pws1  15401  opprval  15408  crngoppr  15411  dvdsrval  15429  isunit  15441  invrfval  15457  dvrfval  15468  isirred  15483  dfrhm2  15500  pwsco1rhm  15512  pwsco2rhm  15513  isdrng  15518  isdrng2  15524  drngid  15528  isdrngrd  15540  issubrg  15547  abvfval  15585  abvneg  15601  staffval  15614  issrng  15617  issrngd  15628  islmod  15633  scaffval  15647  lssset  15693  prdsvscacl  15727  lspfval  15732  islmhm  15786  islmhm2  15797  islmim  15817  islbs  15831  islvec  15859  2idlval  15987  crng2idl  15993  isnzr  16013  rrgval  16030  isdomn  16037  isassa  16058  aspval  16070  asclfval  16076  psrval  16112  mvrfval  16167  mplval  16175  mplcoe3  16212  mplcoe2  16213  ltbval  16215  opsrval  16218  mplind  16245  vr1cl2  16274  ply1val  16275  psropprmul  16318  coe1mul2lem2  16347  coe1tm  16351  coe1sclmul  16360  coe1sclmul2  16362  ply1scl1  16369  ply1coe  16370  mulgrhm2  16463  zlmval  16472  chrval  16481  znval  16491  znzrhfo  16503  znle2  16509  znunithash  16520  cygznlem1  16522  isphl  16534  phllmhm  16538  ipffval  16554  ocvfval  16568  cssval  16584  cssincl  16590  thlval  16597  pjfval  16608  ishil  16620  isobs  16622  istps  16676  cldval  16762  ntrfval  16763  clsfval  16764  neifval  16838  lpfval  16872  isperf  16884  restbas  16891  tgrest  16892  resstopn  16918  ordtval  16921  ordtuni  16922  ordtbas  16924  ordtrest2  16936  ist0  17050  ist1  17051  ishaus  17052  iscnrm  17053  pnrmopn  17073  iscmp  17117  cmpcld  17131  hauscmplem  17135  cmpfi  17137  iscon  17141  consuba  17148  is1stc  17169  txval  17261  ptval  17267  ptbasin  17274  ptbasfi  17278  xkoval  17284  ptunimpt  17292  ptval2  17298  txbasval  17303  dfac14  17314  upxp  17319  uptx  17321  prdstopn  17324  txrest  17327  ptrescn  17335  lmcn2  17345  xkoptsub  17350  xkopt  17351  xkococn  17356  cnmpt2t  17369  cnmpt2res  17373  cnmpt2k  17384  qtopval  17388  imastopn  17413  hmphindis  17490  ptuncnv  17500  ptunhmeo  17501  xpstopnlem1  17502  xpstopnlem2  17504  xkohmeo  17508  qtophmeo  17510  elmptrab  17524  trfbas2  17540  trfil2  17584  fmco  17658  flimval  17660  flfcnp2  17704  fclsval  17705  fclsrest  17721  alexsublem  17740  alexsubALTlem3  17745  alexsubALTlem4  17746  ptcmplem1  17748  ptcmplem3  17750  ptcmpg  17753  istmd  17759  istgp  17762  istgp2  17776  tgplacthmeo  17788  clssubg  17793  tgpconcompeqg  17796  tsmsval2  17814  istrg  17848  istdrg  17850  istlm  17869  istvc  17876  imasdsf1olem  17939  xpsxmetlem  17945  xpsmet  17948  isxms  17995  isms  17997  tmsval  18029  stdbdxmet  18063  prdsxmslem2  18077  txmetcnp  18095  nmfval  18113  isngp  18120  tngval  18157  tngtopn  18168  tngnm  18169  isnrg  18173  isnlm  18188  nmofval  18225  nghmfval  18233  qtopbaslem  18269  cnblcld  18286  negcncf  18423  negfcncf  18424  cncfcnvcn  18426  cnmptre  18427  cnheiborlem  18454  cnheibor  18455  bndth  18458  pcorev2  18528  om1bas  18531  pi1val  18537  pi1bas3  18543  pi1cpbl  18544  pi1xfrcnv  18557  isclm  18564  nmoleub2lem3  18598  nmoleub3  18602  iscph  18608  cphcjcl  18621  tchval  18652  ipcau2  18666  csscld  18678  iscmet  18712  caubl  18735  caublcls  18736  bcthlem4  18751  bcthlem5  18752  bcth3  18755  isbn  18762  iscms  18769  ovolfioo  18829  ovolficc  18830  ovolficcss  18831  ovolfsval  18832  ovolval  18835  ovollb2lem  18849  ovolctb  18851  ovolunlem1a  18857  ovoliunlem1  18863  ovoliun2  18867  shft2rab  18869  ovolshftlem1  18870  sca2rab  18873  ovolscalem1  18874  ovolicc2lem1  18878  ovolicc2lem4  18881  ovolicc2lem5  18882  cmmbl  18894  unmbl  18897  voliunlem3  18911  iunmbl  18912  voliun  18913  ioombl1lem3  18919  ovolfs2  18928  ioorinv  18933  uniiccdif  18935  uniioovol  18936  uniioombllem2a  18939  uniioombllem2  18940  uniioombllem3a  18941  uniioombllem3  18942  uniioombllem4  18943  uniioombllem5  18944  uniioombllem6  18945  dyadovol  18950  dyadss  18951  dyaddisjlem  18952  dyadmaxlem  18954  dyadmbl  18957  opnmbllem  18958  vitalilem4  18968  ismbf  18987  mbfconst  18992  itg2val  19085  itg2monolem1  19107  itg2i1fseq  19112  dfitg  19126  itgz  19137  itgvallem3  19142  iblcnlem1  19144  iblcnlem  19145  iblposlem  19148  itgreval  19153  itgfsum  19183  bddmulibl  19195  itgcn  19199  limcfval  19224  ellimc  19225  limcmpt2  19236  limccnp  19243  dvfval  19249  eldv  19250  dvreslem  19261  dvres2lem  19262  dvidlem  19267  dvnfval  19273  dvexp2  19305  dvrec  19306  dveflem  19328  dvlipcn  19343  dv11cn  19350  lhop  19365  ftc2  19393  evlsval  19405  evlsval2  19406  evlval  19410  evlrhm  19411  evl1fval  19412  evl1sca  19415  evl1var  19417  pf1subrg  19433  pf1ind  19440  mdegfval  19450  uc1pval  19527  mon1pval  19529  q1pval  19541  r1pval  19544  ig1pval  19560  plyconst  19590  plyeq0lem  19594  dgrval  19612  plyco  19625  0dgrb  19630  coemullem  19633  coe0  19639  coesub  19640  dgrsub  19655  dgrcolem1  19656  dgrcolem2  19657  dgrco  19658  quotval  19674  plydivex  19679  quotlem  19682  plyremlem  19686  fta1  19690  vieta1lem1  19692  vieta1lem2  19693  vieta1  19694  aaliou2  19722  aaliou3lem7  19731  taylpfval  19746  dvtaylp  19751  dvntaylp0  19753  taylthlem1  19754  ulm2  19766  ulmshft  19771  pserdvlem2  19806  abelthlem1  19809  abelthlem8  19817  abelth  19819  abelth2  19820  ptolemy  19866  coskpi  19890  efif1olem2  19907  efif1olem3  19908  logcnlem4  19994  advlogexp  20004  efopn  20007  logtayl  20009  dcubic2  20142  dcubic  20144  quart1lem  20153  atancj  20208  tanatan  20217  cosatan  20219  dvatan  20233  leibpi  20240  birthdaylem2  20249  efrlim  20266  emcllem7  20297  wilthlem2  20309  basellem5  20324  basellem8  20327  basellem9  20328  vmaval  20353  prmorcht  20418  mumul  20421  dvdsmulf1o  20436  fsumdvdsmul  20437  ppiub  20445  fsumvma  20454  pclogsum  20456  dchrval  20475  bposlem8  20532  lgslem1  20537  lgsval  20541  lgsval4  20557  lgsfcl3  20558  lgsdilem  20563  lgsdir2lem4  20567  lgsdir2lem5  20568  lgsquadlem2  20596  dchrisum0flb  20661  rpvmasum2  20663  log2sumbnd  20695  selberglem2  20697  pntibndlem2  20742  pntlemp  20761  ostth2lem3  20786  ostth2lem4  20787  isplig  20846  gidval  20882  grpoinvfval  20893  grpodivfval  20911  gxfval  20926  isablo  20952  subgornss  20975  isexid  20986  elghomlem1  21030  isrngo  21047  drngoi  21076  vci  21106  isvclem  21135  nvop2  21166  nvvop  21167  isnvlem  21168  dipfval  21277  sspval  21301  isssp  21302  lnoval  21332  nmoofval  21342  bloval  21361  0ofval  21367  ajfval  21389  hmoval  21390  isphg  21397  phop  21398  ipasslem11  21420  siii  21433  iscbn  21445  opsqrlem6  22727  elpjrn  22772  hstle1  22808  stm1addi  22827  stm1add3i  22829  mdslmd1lem1  22907  mdexchi  22917  atordi  22966  dmdbr5ati  23004  cdj3lem1  23016  feqmptdf  23230  xrofsup  23257  xpinpreima2  23293  xrge0mulc1cn  23325  disjabrex  23361  disjabrexf  23362  esumsn  23439  ofcc  23469  sxval  23523  measvuni  23544  itgmeq123dTMP  23591  totprob  23632  orrvcval4  23667  subfacp1lem5  23717  subfacp1lem6  23718  ispcon  23756  pconpi1  23770  rescon  23779  iscvm  23792  cvmsss2  23807  cvmliftlem3  23820  cvmliftlem5  23822  cvmliftlem10  23827  cvmliftlem11  23828  cvmlift2lem9a  23836  cvmlift2lem2  23837  cvmliftphtlem  23850  cvmlift3lem7  23858  umgraex  23877  vdgr1d  23896  eupath2lem3  23905  snmlflim  23917  ghomgrpilem2  23995  fz0n  24099  rdgprc  24153  dfrdg2  24154  dftrpred4g  24239  dfrdg4  24490  colinearalglem4  24539  axlowdimlem3  24574  axlowdimlem16  24587  axlowdimlem17  24588  fvline2  24771  ellines  24777  bpolylem  24785  bpoly1  24788  bpolydiflem  24791  rankeq1o  24803  ordcmp  24888  dvreasin  24925  dvreacos  24926  itg2addnclem  24933  areacirclem2  24936  areacirclem6  24941  dfoprab4pop  25048  fnovpop  25049  prjdmn  25093  prjrn  25094  mapex2  25151  repfuntw  25171  iscst1  25185  valcurfn1  25215  isorhom  25222  gepsup  25261  seinf  25262  mxlelt  25275  ltrcmp  25416  com2i  25427  idlvalNEW  25456  vri  25503  istopxc  25559  prdnei  25584  limptlimpr2lem2  25586  islimrs  25591  isalg  25732  algi  25738  isded  25747  dedi  25748  dedalg  25754  iscatOLD  25765  cati  25766  catded  25775  ishoma  25798  ismona  25820  isepia  25830  isiso  25836  cinvlem1  25839  isfuna  25845  issubcat  25856  linevala2  26089  isray2  26164  clsun  26257  isfne  26279  isref  26290  isptfin  26306  islocfin  26307  neibastop3  26322  cover2g  26370  f1opr  26402  sdclem1  26464  sstotbnd  26510  ssbnd  26523  prdstotbnd  26529  prdsbnd2  26530  ismtyhmeolem  26539  heiborlem3  26548  heiborlem4  26549  heiborlem6  26551  rrnval  26562  rrncmslem  26567  ismrer1  26573  reheibor  26574  rngohomval  26606  rngoisoval  26619  idlval  26649  pridlval  26669  maxidlval  26675  isprrngo  26686  igenval  26697  fndifnfp  26767  elrfi  26780  isnacs  26790  ofmpteq  26808  diophin  26863  dnnumch1  27152  islmodfg  27178  islnm  27186  lnmlssfg  27189  dsmmval  27211  dsmmbas2  27214  dsmmfi  27215  dsmm0cl  27217  frlmpws  27229  frlmlss  27230  frlmbas  27234  uvcfval  27244  frlmsplit2  27254  mapfien2  27269  frlmpwfi  27273  islindf  27293  lindfmm  27308  islindf5  27320  hbtlem1  27338  hbtlem7  27340  hbtlem6  27344  dgrnznn  27351  pmtrmvd  27409  pmtrfrn  27411  psgnunilem2  27429  psgnfval  27434  psgnghm2  27449  mamufval  27454  matval  27476  matplusg2  27488  matvsca2  27489  mdetfval  27498  mendval  27502  mendplusgfval  27504  mendmulrfval  27506  mendvscafval  27509  fgraphxp  27541  iotain  27628  rfcnpre1  27701  rfcnpre2  27713  rfcnpre3  27715  rfcnpre4  27716  fmuldfeq  27724  itgsinexplem1  27759  stoweidlem34  27794  stoweidlem41  27801  dfafn5a  28033  dfaimafn2  28039  ffnaov  28070  usgraexvlem  28138  1to2vfriswmgra  28195  dpval  28251  bnj66  28965  bnj570  29010  bnj1326  29129  bnj1463  29158  bnj1501  29170  lshpset  29241  lsatset  29253  lcvfbr  29283  lflset  29322  lkrfval  29350  lkrval2  29353  ldualset  29388  isopos  29443  cmtfvalN  29473  isoml  29501  cvrfval  29531  pats  29548  isatl  29562  iscvlat  29586  ishlat1  29615  llnset  29767  lplnset  29791  lvolset  29834  dalem58  29992  dalem59  29993  lineset  30000  pointsetN  30003  psubspset  30006  pmapfval  30018  paddfval  30059  pclfvalN  30151  polfvalN  30166  psubclsetN  30198  watfvalN  30254  lhpset  30257  lautset  30344  pautsetN  30360  ldilfset  30370  ltrnfset  30379  ltrnset  30380  ltrncoidN  30390  dilfsetN  30414  trnfsetN  30417  trlfset  30422  trlset  30423  cdleme6  30503  cdleme11g  30527  cdleme31sn1  30643  cdleme31sn1c  30650  cdleme31sn2  30651  cdleme40v  30731  cdleme42ke  30747  cdleme50trn2a  30812  cdleme50trn3  30815  cdlemg1b2  30833  cdlemg47  30998  tgrpfset  31006  tgrpset  31007  tendofset  31020  tendoset  31021  erngfset  31061  erngset  31062  erngfset-rN  31069  erngset-rN  31070  cdlemi  31082  cdlemk4  31096  cdlemkuu  31157  cdlemk35  31174  cdlemky  31188  cdlemk54  31220  cdlemk55a  31221  cdlemkyyN  31224  dva1dim  31247  erngdvlem3-rN  31260  dvafset  31266  dvaset  31267  diaffval  31293  diafval  31294  diaintclN  31321  dvhfset  31343  dvhset  31344  cdlemm10N  31381  docaffvalN  31384  docafvalN  31385  djaffvalN  31396  djafvalN  31397  dibffval  31403  dibfval  31404  dib1dim  31428  dibintclN  31430  dicffval  31437  dicfval  31438  dicval2  31442  dihffval  31493  dihfval  31494  dihopelvalcpre  31511  dihmeetbclemN  31567  dih1dimatlem  31592  dihglb2  31605  dihintcl  31607  dochffval  31612  dochfval  31613  djhffval  31659  djhfval  31660  dihjatcclem1  31681  dihjatcclem3  31683  djhlsmat  31690  lpolsetN  31745  lcdfval  31851  lcdval  31852  lcdval2  31853  lcdsca  31862  mapdffval  31889  mapdfval  31890  mapdval3N  31894  mapdval5N  31896  mapdpglem21  31955  hvmapffval  32021  hvmapfval  32022  hdmap1ffval  32059  hdmap1fval  32060  hdmapffval  32092  hdmapfval  32093  hgmapffval  32151  hgmapfval  32152  hdmapoc  32197  hlhilset  32200  hlhilslem  32204  hlhilnvl  32216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-cleq 2278
  Copyright terms: Public domain W3C validator