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

Theorem syl6eqr 2346
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 2300 . 2  |-  B  =  C
41, 3syl6eq 2344 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  3eqtr4g  2353  iinrab2  3981  relop  4850  dfiun3g  4947  dfiin3g  4948  resima2  5004  relcnvfld  5219  uniabio  5245  iotanul  5250  dffn5  5584  dfimafn2  5588  fncnvima2  5663  fmptcof  5708  fcoconst  5711  resfunexg  5753  ffnov  5964  fnov  5968  fnrnov  6009  foov  6010  funimassov  6013  ovelimab  6014  ofc12  6118  caofinvl  6120  1st2val  6161  2nd2val  6162  curry1  6226  curry2  6229  dftpos3  6268  riotav  6325  riotauni  6327  tz7.44-3  6437  rdgsucmptnf  6458  rdglim2a  6462  frsucmptn  6467  seqomlem1  6478  seqomlem4  6481  oa0r  6553  om1r  6557  oarec  6576  oacomf1olem  6578  oeeulem  6615  omabs  6661  ecinxp  6750  mapunen  7046  phplem1  7056  fodomfi  7151  iinfi  7187  fiin  7191  dffi3  7200  ordtypelem3  7251  ordtypelem9  7257  cantnffval  7380  cantnfval  7385  cantnfp1lem3  7398  cantnflem1  7407  wemapwe  7416  oef1o  7417  cnfcom2lem  7420  rankuni  7551  cardval2  7640  dfac8alem  7672  dfac12lem1  7785  cda1dif  7818  cdaassen  7824  isf34lem4  8019  hsmexlem5  8072  axdc3lem4  8095  axdc4lem  8097  ac6num  8122  zorn2lem1  8139  ttukeylem3  8154  pwcfsdom  8221  fpwwe2lem9  8276  canth4  8285  canthp1lem2  8291  genpass  8649  prlem934  8673  mulcmpblnrlem  8711  recexsrlem  8741  supsrlem  8749  axrnegex  8800  nneo  10111  cnref1o  10365  xmulneg1  10605  xmulpnf1n  10614  xadddi  10631  fztp  10857  fseq1m1p1  10874  uzrdgsuci  11039  mulexpz  11158  expaddz  11162  bcp1m1  11348  seqcoll  11417  iswrdi  11433  cjexp  11651  rexuz3  11848  limsupval  11964  limsupgle  11967  climconst  12033  zsum  12207  fsum  12209  sum0  12210  sumz  12211  fsumcnv  12252  incexc2  12313  mertenslem2  12357  efval2  12381  ege2le3  12387  efzval  12398  efival  12448  sinbnd  12476  cosbnd  12477  sadfval  12659  bitsres  12680  smufval  12684  smupp1  12687  eucalgval  12768  eucalginv  12770  eucalglt  12771  eucalgcvga  12772  eucalg  12773  dfphi2  12858  phimullem  12863  prmdiv  12869  odzval  12872  pcval  12913  pczpre  12916  pcrec  12927  prmreclem6  12984  4sqlem17  13024  vdwmc  13041  vdwpc  13043  vdwlem8  13051  ramval  13071  ramcl  13092  ressval  13211  resslem  13217  firest  13353  topnval  13355  prdsval  13371  prdsleval  13392  prdsbas3  13396  prdsdsval2  13399  pwsval  13401  pwsbas  13402  pwselbasb  13403  pwsplusgval  13405  pwsmulrval  13406  pwsle  13407  pwsvscafval  13409  imasval  13430  imasdsval  13434  imasdsval2  13435  divsval  13460  xpsval  13490  xpslem  13491  xpsaddlem  13493  xpsvsca  13497  xpsle  13499  mrisval  13548  iscat  13590  cidfval  13594  homffval  13610  comfffval  13617  comffval  13618  comfeq  13625  oppcval  13632  oppchomfval  13633  oppccofval  13635  oppcbas  13637  oppcid  13640  monfval  13651  oppcmon  13657  sectffval  13669  invffval  13676  isoval  13683  isssc  13713  rescbas  13722  reschomf  13724  issubc  13728  isfunc  13754  isfuncd  13755  funcf2  13758  idfuval  13766  idfu2nd  13767  cofucl  13778  resfval2  13783  resf2nd  13785  funcres2b  13787  funcpropd  13790  isfull  13800  isfth  13804  natfval  13836  fucval  13848  fuccofval  13849  fucbas  13850  fuchom  13851  homafval  13877  homaval  13879  homadmcd  13890  arwval  13891  arwhoma  13893  idafval  13905  coafval  13912  coapm  13919  catcco  13949  catcid  13951  catcisolem  13954  xpcval  13967  xpcco  13973  1stfval  13981  2ndfval  13984  xpcpropd  13998  evlfval  14007  evlfcllem  14011  evlfcl  14012  curfval  14013  curf1cl  14018  curfcl  14022  uncf1  14026  uncf2  14027  uncfcurf  14029  diag2  14035  curf2ndf  14037  hofval  14042  hof2fval  14045  hofcl  14049  yonval  14051  hofpropd  14057  yonedalem21  14063  yonedalem22  14068  yonedalem3  14070  yonedainv  14071  yonffthlem  14072  isdrs  14084  ispos  14097  pltfval  14109  lubfval  14128  glbfval  14133  joinfval  14137  meetfval  14144  p0val  14163  p1val  14164  islat  14169  isclat  14231  ipoval  14273  isipodrs  14280  isdlat  14312  istsr  14342  spwval2  14349  isla  14358  isdir  14370  ismnd  14385  plusffval  14395  grpidval  14400  ismgmid  14403  pws0g  14424  ismhm  14433  submacs  14458  gsumvalx  14467  frmdval  14489  isgrp  14509  grpn0  14530  grpinvfval  14536  grpsubfval  14540  mulgfval  14584  mulgval  14585  mulgnn0p1  14594  pwsinvg  14623  issubg  14637  isnsg  14662  eqgfval  14681  divseccl  14689  isghm  14699  conjsubg  14730  conjsubgen  14731  isgim  14742  isga  14761  symgval  14787  cntrval  14811  cntzfval  14812  oppgval  14836  invoppggim  14849  odfval  14864  odval  14865  gexval  14905  ispgp  14919  sylow1lem1  14925  slwispgp  14938  pgpssslw  14941  sylow2alem2  14945  sylow3lem5  14958  lsmfval  14965  pj1fval  15019  efgmnvl  15039  efgval  15042  efgval2  15049  efginvrel2  15052  efgsfo  15064  efgredleme  15068  efgredlemd  15069  efgredlemc  15070  frgpval  15083  frgpeccl  15086  vrgpfval  15091  frgpuptinv  15096  frgpup3lem  15102  iscmn  15112  subcmn  15149  frgpnabllem1  15177  iscyg  15182  lt6abl  15197  gsumval3  15207  gsumzf1o  15212  gsum2d  15239  gsumcom2  15242  dmdprd  15252  dprdval  15254  dprd2da  15293  dmdprdsplit2lem  15296  dpjfval  15306  pgpfaclem1  15332  mgpval  15344  mgpplusg  15345  isrng  15361  iscrng  15364  pws1  15415  opprval  15422  crngoppr  15425  dvdsrval  15443  isunit  15455  invrfval  15471  dvrfval  15482  isirred  15497  dfrhm2  15514  pwsco1rhm  15526  pwsco2rhm  15527  isdrng  15532  isdrng2  15538  drngid  15542  isdrngrd  15554  issubrg  15561  abvfval  15599  abvneg  15615  staffval  15628  issrng  15631  issrngd  15642  islmod  15647  scaffval  15661  lssset  15707  prdsvscacl  15741  lspfval  15746  islmhm  15800  islmhm2  15811  islmim  15831  islbs  15845  islvec  15873  2idlval  16001  crng2idl  16007  isnzr  16027  rrgval  16044  isdomn  16051  isassa  16072  aspval  16084  asclfval  16090  psrval  16126  mvrfval  16181  mplval  16189  mplcoe3  16226  mplcoe2  16227  ltbval  16229  opsrval  16232  mplind  16259  vr1cl2  16288  ply1val  16289  psropprmul  16332  coe1mul2lem2  16361  coe1tm  16365  coe1sclmul  16374  coe1sclmul2  16376  ply1scl1  16383  ply1coe  16384  mulgrhm2  16477  zlmval  16486  chrval  16495  znval  16505  znzrhfo  16517  znle2  16523  znunithash  16534  cygznlem1  16536  isphl  16548  phllmhm  16552  ipffval  16568  ocvfval  16582  cssval  16598  cssincl  16604  thlval  16611  pjfval  16622  ishil  16634  isobs  16636  istps  16690  cldval  16776  ntrfval  16777  clsfval  16778  neifval  16852  lpfval  16886  isperf  16898  restbas  16905  tgrest  16906  resstopn  16932  ordtval  16935  ordtuni  16936  ordtbas  16938  ordtrest2  16950  ist0  17064  ist1  17065  ishaus  17066  iscnrm  17067  pnrmopn  17087  iscmp  17131  cmpcld  17145  hauscmplem  17149  cmpfi  17151  iscon  17155  consuba  17162  is1stc  17183  txval  17275  ptval  17281  ptbasin  17288  ptbasfi  17292  xkoval  17298  ptunimpt  17306  ptval2  17312  txbasval  17317  dfac14  17328  upxp  17333  uptx  17335  prdstopn  17338  txrest  17341  ptrescn  17349  lmcn2  17359  xkoptsub  17364  xkopt  17365  xkococn  17370  cnmpt2t  17383  cnmpt2res  17387  cnmpt2k  17398  qtopval  17402  imastopn  17427  hmphindis  17504  ptuncnv  17514  ptunhmeo  17515  xpstopnlem1  17516  xpstopnlem2  17518  xkohmeo  17522  qtophmeo  17524  elmptrab  17538  trfbas2  17554  trfil2  17598  fmco  17672  flimval  17674  flfcnp2  17718  fclsval  17719  fclsrest  17735  alexsublem  17754  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem1  17762  ptcmplem3  17764  ptcmpg  17767  istmd  17773  istgp  17776  istgp2  17790  tgplacthmeo  17802  clssubg  17807  tgpconcompeqg  17810  tsmsval2  17828  istrg  17862  istdrg  17864  istlm  17883  istvc  17890  imasdsf1olem  17953  xpsxmetlem  17959  xpsmet  17962  isxms  18009  isms  18011  tmsval  18043  stdbdxmet  18077  prdsxmslem2  18091  txmetcnp  18109  nmfval  18127  isngp  18134  tngval  18171  tngtopn  18182  tngnm  18183  isnrg  18187  isnlm  18202  nmofval  18239  nghmfval  18247  qtopbaslem  18283  cnblcld  18300  negcncf  18437  negfcncf  18438  cncfcnvcn  18440  cnmptre  18441  cnheiborlem  18468  cnheibor  18469  bndth  18472  pcorev2  18542  om1bas  18545  pi1val  18551  pi1bas3  18557  pi1cpbl  18558  pi1xfrcnv  18571  isclm  18578  nmoleub2lem3  18612  nmoleub3  18616  iscph  18622  cphcjcl  18635  tchval  18666  ipcau2  18680  csscld  18692  iscmet  18726  caubl  18749  caublcls  18750  bcthlem4  18765  bcthlem5  18766  bcth3  18769  isbn  18776  iscms  18783  ovolfioo  18843  ovolficc  18844  ovolficcss  18845  ovolfsval  18846  ovolval  18849  ovollb2lem  18863  ovolctb  18865  ovolunlem1a  18871  ovoliunlem1  18877  ovoliun2  18881  shft2rab  18883  ovolshftlem1  18884  sca2rab  18887  ovolscalem1  18888  ovolicc2lem1  18892  ovolicc2lem4  18895  ovolicc2lem5  18896  cmmbl  18908  unmbl  18911  voliunlem3  18925  iunmbl  18926  voliun  18927  ioombl1lem3  18933  ovolfs2  18942  ioorinv  18947  uniiccdif  18949  uniioovol  18950  uniioombllem2a  18953  uniioombllem2  18954  uniioombllem3a  18955  uniioombllem3  18956  uniioombllem4  18957  uniioombllem5  18958  uniioombllem6  18959  dyadovol  18964  dyadss  18965  dyaddisjlem  18966  dyadmaxlem  18968  dyadmbl  18971  opnmbllem  18972  vitalilem4  18982  ismbf  19001  mbfconst  19006  itg2val  19099  itg2monolem1  19121  itg2i1fseq  19126  dfitg  19140  itgz  19151  itgvallem3  19156  iblcnlem1  19158  iblcnlem  19159  iblposlem  19162  itgreval  19167  itgfsum  19197  bddmulibl  19209  itgcn  19213  limcfval  19238  ellimc  19239  limcmpt2  19250  limccnp  19257  dvfval  19263  eldv  19264  dvreslem  19275  dvres2lem  19276  dvidlem  19281  dvnfval  19287  dvexp2  19319  dvrec  19320  dveflem  19342  dvlipcn  19357  dv11cn  19364  lhop  19379  ftc2  19407  evlsval  19419  evlsval2  19420  evlval  19424  evlrhm  19425  evl1fval  19426  evl1sca  19429  evl1var  19431  pf1subrg  19447  pf1ind  19454  mdegfval  19464  uc1pval  19541  mon1pval  19543  q1pval  19555  r1pval  19558  ig1pval  19574  plyconst  19604  plyeq0lem  19608  dgrval  19626  plyco  19639  0dgrb  19644  coemullem  19647  coe0  19653  coesub  19654  dgrsub  19669  dgrcolem1  19670  dgrcolem2  19671  dgrco  19672  quotval  19688  plydivex  19693  quotlem  19696  plyremlem  19700  fta1  19704  vieta1lem1  19706  vieta1lem2  19707  vieta1  19708  aaliou2  19736  aaliou3lem7  19745  taylpfval  19760  dvtaylp  19765  dvntaylp0  19767  taylthlem1  19768  ulm2  19780  ulmshft  19785  pserdvlem2  19820  abelthlem1  19823  abelthlem8  19831  abelth  19833  abelth2  19834  ptolemy  19880  coskpi  19904  efif1olem2  19921  efif1olem3  19922  logcnlem4  20008  advlogexp  20018  efopn  20021  logtayl  20023  dcubic2  20156  dcubic  20158  quart1lem  20167  atancj  20222  tanatan  20231  cosatan  20233  dvatan  20247  leibpi  20254  birthdaylem2  20263  efrlim  20280  emcllem7  20311  wilthlem2  20323  basellem5  20338  basellem8  20341  basellem9  20342  vmaval  20367  prmorcht  20432  mumul  20435  dvdsmulf1o  20450  fsumdvdsmul  20451  ppiub  20459  fsumvma  20468  pclogsum  20470  dchrval  20489  bposlem8  20546  lgslem1  20551  lgsval  20555  lgsval4  20571  lgsfcl3  20572  lgsdilem  20577  lgsdir2lem4  20581  lgsdir2lem5  20582  lgsquadlem2  20610  dchrisum0flb  20675  rpvmasum2  20677  log2sumbnd  20709  selberglem2  20711  pntibndlem2  20756  pntlemp  20775  ostth2lem3  20800  ostth2lem4  20801  isplig  20860  gidval  20896  grpoinvfval  20907  grpodivfval  20925  gxfval  20940  isablo  20966  subgornss  20989  isexid  21000  elghomlem1  21044  isrngo  21061  drngoi  21090  vci  21120  isvclem  21149  nvop2  21180  nvvop  21181  isnvlem  21182  dipfval  21291  sspval  21315  isssp  21316  lnoval  21346  nmoofval  21356  bloval  21375  0ofval  21381  ajfval  21403  hmoval  21404  isphg  21411  phop  21412  ipasslem11  21434  siii  21447  iscbn  21459  opsqrlem6  22741  elpjrn  22786  hstle1  22822  stm1addi  22841  stm1add3i  22843  mdslmd1lem1  22921  mdexchi  22931  atordi  22980  dmdbr5ati  23018  cdj3lem1  23030  feqmptdf  23243  xrofsup  23270  xpinpreima2  23306  xrge0mulc1cn  23338  disjabrex  23374  disjabrexf  23375  esumsn  23452  ofcc  23482  sxval  23536  measvuni  23557  itgmeq123dTMP  23604  totprob  23645  orrvcval4  23680  subfacp1lem5  23730  subfacp1lem6  23731  ispcon  23769  pconpi1  23783  rescon  23792  iscvm  23805  cvmsss2  23820  cvmliftlem3  23833  cvmliftlem5  23835  cvmliftlem10  23840  cvmliftlem11  23841  cvmlift2lem9a  23849  cvmlift2lem2  23850  cvmliftphtlem  23863  cvmlift3lem7  23871  umgraex  23890  vdgr1d  23909  eupath2lem3  23918  snmlflim  23930  ghomgrpilem2  24008  fz0n  24112  zprod  24160  fprod  24164  cprod0  24168  prod1  24169  rdgprc  24222  dfrdg2  24223  dftrpred4g  24308  dfrdg4  24560  colinearalglem4  24609  axlowdimlem3  24644  axlowdimlem16  24657  axlowdimlem17  24658  fvline2  24841  ellines  24847  bpolylem  24855  bpoly1  24858  bpolydiflem  24861  rankeq1o  24873  ordcmp  24958  itg2addnclem  25003  itgaddnclem2  25010  dvreasin  25026  dvreacos  25027  areacirclem2  25028  areacirclem6  25033  dfoprab4pop  25140  fnovpop  25141  prjdmn  25185  prjrn  25186  mapex2  25243  repfuntw  25263  iscst1  25277  valcurfn1  25307  isorhom  25314  gepsup  25353  seinf  25354  mxlelt  25367  ltrcmp  25508  com2i  25519  idlvalNEW  25548  vri  25595  istopxc  25651  prdnei  25676  limptlimpr2lem2  25678  islimrs  25683  isalg  25824  algi  25830  isded  25839  dedi  25840  dedalg  25846  iscatOLD  25857  cati  25858  catded  25867  ishoma  25890  ismona  25912  isepia  25922  isiso  25928  cinvlem1  25931  isfuna  25937  issubcat  25948  linevala2  26181  isray2  26256  clsun  26349  isfne  26371  isref  26382  isptfin  26398  islocfin  26399  neibastop3  26414  cover2g  26462  f1opr  26494  sdclem1  26556  sstotbnd  26602  ssbnd  26615  prdstotbnd  26621  prdsbnd2  26622  ismtyhmeolem  26631  heiborlem3  26640  heiborlem4  26641  heiborlem6  26643  rrnval  26654  rrncmslem  26659  ismrer1  26665  reheibor  26666  rngohomval  26698  rngoisoval  26711  idlval  26741  pridlval  26761  maxidlval  26767  isprrngo  26778  igenval  26789  fndifnfp  26859  elrfi  26872  isnacs  26882  ofmpteq  26900  diophin  26955  dnnumch1  27244  islmodfg  27270  islnm  27278  lnmlssfg  27281  dsmmval  27303  dsmmbas2  27306  dsmmfi  27307  dsmm0cl  27309  frlmpws  27321  frlmlss  27322  frlmbas  27326  uvcfval  27336  frlmsplit2  27346  mapfien2  27361  frlmpwfi  27365  islindf  27385  lindfmm  27400  islindf5  27412  hbtlem1  27430  hbtlem7  27432  hbtlem6  27436  dgrnznn  27443  pmtrmvd  27501  pmtrfrn  27503  psgnunilem2  27521  psgnfval  27526  psgnghm2  27541  mamufval  27546  matval  27568  matplusg2  27580  matvsca2  27581  mdetfval  27590  mendval  27594  mendplusgfval  27596  mendmulrfval  27598  mendvscafval  27601  fgraphxp  27633  iotain  27720  rfcnpre1  27793  rfcnpre2  27805  rfcnpre3  27807  rfcnpre4  27808  fmuldfeq  27816  itgsinexplem1  27851  stoweidlem34  27886  stoweidlem41  27893  dfafn5a  28128  dfaimafn2  28134  ffnaov  28167  usgraexvlem  28261  constr3trllem3  28398  constr3cycllem1  28404  1to2vfriswmgra  28430  dpval  28494  bnj66  29208  bnj570  29253  bnj1326  29372  bnj1463  29401  bnj1501  29413  lshpset  29790  lsatset  29802  lcvfbr  29832  lflset  29871  lkrfval  29899  lkrval2  29902  ldualset  29937  isopos  29992  cmtfvalN  30022  isoml  30050  cvrfval  30080  pats  30097  isatl  30111  iscvlat  30135  ishlat1  30164  llnset  30316  lplnset  30340  lvolset  30383  dalem58  30541  dalem59  30542  lineset  30549  pointsetN  30552  psubspset  30555  pmapfval  30567  paddfval  30608  pclfvalN  30700  polfvalN  30715  psubclsetN  30747  watfvalN  30803  lhpset  30806  lautset  30893  pautsetN  30909  ldilfset  30919  ltrnfset  30928  ltrnset  30929  ltrncoidN  30939  dilfsetN  30963  trnfsetN  30966  trlfset  30971  trlset  30972  cdleme6  31052  cdleme11g  31076  cdleme31sn1  31192  cdleme31sn1c  31199  cdleme31sn2  31200  cdleme40v  31280  cdleme42ke  31296  cdleme50trn2a  31361  cdleme50trn3  31364  cdlemg1b2  31382  cdlemg47  31547  tgrpfset  31555  tgrpset  31556  tendofset  31569  tendoset  31570  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  cdlemi  31631  cdlemk4  31645  cdlemkuu  31706  cdlemk35  31723  cdlemky  31737  cdlemk54  31769  cdlemk55a  31770  cdlemkyyN  31773  dva1dim  31796  erngdvlem3-rN  31809  dvafset  31815  dvaset  31816  diaffval  31842  diafval  31843  diaintclN  31870  dvhfset  31892  dvhset  31893  cdlemm10N  31930  docaffvalN  31933  docafvalN  31934  djaffvalN  31945  djafvalN  31946  dibffval  31952  dibfval  31953  dib1dim  31977  dibintclN  31979  dicffval  31986  dicfval  31987  dicval2  31991  dihffval  32042  dihfval  32043  dihopelvalcpre  32060  dihmeetbclemN  32116  dih1dimatlem  32141  dihglb2  32154  dihintcl  32156  dochffval  32161  dochfval  32162  djhffval  32208  djhfval  32209  dihjatcclem1  32230  dihjatcclem3  32232  djhlsmat  32239  lpolsetN  32294  lcdfval  32400  lcdval  32401  lcdval2  32402  lcdsca  32411  mapdffval  32438  mapdfval  32439  mapdval3N  32443  mapdval5N  32445  mapdpglem21  32504  hvmapffval  32570  hvmapfval  32571  hdmap1ffval  32608  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701  hdmapoc  32746  hlhilset  32749  hlhilslem  32753  hlhilnvl  32765
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator