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

Theorem syl6eqr 2334
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 2288 . 2  |-  B  =  C
41, 3syl6eq 2332 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  3eqtr4g  2341  iinrab2  3966  relop  4833  dfiun3g  4930  dfiin3g  4931  resima2  4987  relcnvfld  5201  dffn5  5530  dfimafn2  5534  fncnvima2  5609  fmptcof  5654  fcoconst  5657  resfunexg  5699  ffnov  5910  fnov  5914  fnrnov  5955  foov  5956  funimassov  5959  ovelimab  5960  ofc12  6064  caofinvl  6066  1st2val  6107  2nd2val  6108  curry1  6172  curry2  6175  dftpos3  6214  uniabio  6263  iotanul  6268  riotav  6305  riotauni  6307  tz7.44-3  6417  rdgsucmptnf  6438  rdglim2a  6442  frsucmptn  6447  seqomlem1  6458  seqomlem4  6461  oa0r  6533  om1r  6537  oarec  6556  oacomf1olem  6558  oeeulem  6595  omabs  6641  ecinxp  6730  mapunen  7026  phplem1  7036  fodomfi  7131  iinfi  7167  fiin  7171  dffi3  7180  ordtypelem3  7231  ordtypelem9  7237  cantnffval  7360  cantnfval  7365  cantnfp1lem3  7378  cantnflem1  7387  wemapwe  7396  oef1o  7397  cnfcom2lem  7400  rankuni  7531  cardval2  7620  dfac8alem  7652  dfac12lem1  7765  cda1dif  7798  cdaassen  7804  isf34lem4  7999  hsmexlem5  8052  axdc3lem4  8075  axdc4lem  8077  ac6num  8102  zorn2lem1  8119  ttukeylem3  8134  pwcfsdom  8201  fpwwe2lem9  8256  canth4  8265  canthp1lem2  8271  genpass  8629  prlem934  8653  mulcmpblnrlem  8691  recexsrlem  8721  supsrlem  8729  axrnegex  8780  nneo  10091  cnref1o  10345  xmulneg1  10585  xmulpnf1n  10594  xadddi  10611  fztp  10837  fseq1m1p1  10854  uzrdgsuci  11019  mulexpz  11138  expaddz  11142  bcp1m1  11328  seqcoll  11397  iswrdi  11413  cjexp  11631  rexuz3  11828  limsupval  11944  limsupgle  11947  climconst  12013  zsum  12187  fsum  12189  sum0  12190  sumz  12191  fsumcnv  12232  incexc2  12293  mertenslem2  12337  efval2  12361  ege2le3  12367  efzval  12378  efival  12428  sinbnd  12456  cosbnd  12457  sadfval  12639  bitsres  12660  smufval  12664  smupp1  12667  eucalgval  12748  eucalginv  12750  eucalglt  12751  eucalgcvga  12752  eucalg  12753  dfphi2  12838  phimullem  12843  prmdiv  12849  odzval  12852  pcval  12893  pczpre  12896  pcrec  12907  prmreclem6  12964  4sqlem17  13004  vdwmc  13021  vdwpc  13023  vdwlem8  13031  ramval  13051  ramcl  13072  ressval  13191  resslem  13197  firest  13333  topnval  13335  prdsval  13351  prdsleval  13372  prdsbas3  13376  prdsdsval2  13379  pwsval  13381  pwsbas  13382  pwselbasb  13383  pwsplusgval  13385  pwsmulrval  13386  pwsle  13387  pwsvscafval  13389  imasval  13410  imasdsval  13414  imasdsval2  13415  divsval  13440  xpsval  13470  xpslem  13471  xpsaddlem  13473  xpsvsca  13477  xpsle  13479  mrisval  13528  iscat  13570  cidfval  13574  homffval  13590  comfffval  13597  comffval  13598  comfeq  13605  oppcval  13612  oppchomfval  13613  oppccofval  13615  oppcbas  13617  oppcid  13620  monfval  13631  oppcmon  13637  sectffval  13649  invffval  13656  isoval  13663  isssc  13693  rescbas  13702  reschomf  13704  issubc  13708  isfunc  13734  isfuncd  13735  funcf2  13738  idfuval  13746  idfu2nd  13747  cofucl  13758  resfval2  13763  resf2nd  13765  funcres2b  13767  funcpropd  13770  isfull  13780  isfth  13784  natfval  13816  fucval  13828  fuccofval  13829  fucbas  13830  fuchom  13831  homafval  13857  homaval  13859  homadmcd  13870  arwval  13871  arwhoma  13873  idafval  13885  coafval  13892  coapm  13899  catcco  13929  catcid  13931  catcisolem  13934  xpcval  13947  xpcco  13953  1stfval  13961  2ndfval  13964  xpcpropd  13978  evlfval  13987  evlfcllem  13991  evlfcl  13992  curfval  13993  curf1cl  13998  curfcl  14002  uncf1  14006  uncf2  14007  uncfcurf  14009  diag2  14015  curf2ndf  14017  hofval  14022  hof2fval  14025  hofcl  14029  yonval  14031  hofpropd  14037  yonedalem21  14043  yonedalem22  14048  yonedalem3  14050  yonedainv  14051  yonffthlem  14052  isdrs  14064  ispos  14077  pltfval  14089  lubfval  14108  glbfval  14113  joinfval  14117  meetfval  14124  p0val  14143  p1val  14144  islat  14149  isclat  14211  ipoval  14253  isipodrs  14260  isdlat  14292  istsr  14322  spwval2  14329  isla  14338  isdir  14350  ismnd  14365  plusffval  14375  grpidval  14380  ismgmid  14383  pws0g  14404  ismhm  14413  submacs  14438  gsumvalx  14447  frmdval  14469  isgrp  14489  grpn0  14510  grpinvfval  14516  grpsubfval  14520  mulgfval  14564  mulgval  14565  mulgnn0p1  14574  pwsinvg  14603  issubg  14617  isnsg  14642  eqgfval  14661  divseccl  14669  isghm  14679  conjsubg  14710  conjsubgen  14711  isgim  14722  isga  14741  symgval  14767  cntrval  14791  cntzfval  14792  oppgval  14816  invoppggim  14829  odfval  14844  odval  14845  gexval  14885  ispgp  14899  sylow1lem1  14905  slwispgp  14918  pgpssslw  14921  sylow2alem2  14925  sylow3lem5  14938  lsmfval  14945  pj1fval  14999  efgmnvl  15019  efgval  15022  efgval2  15029  efginvrel2  15032  efgsfo  15044  efgredleme  15048  efgredlemd  15049  efgredlemc  15050  frgpval  15063  frgpeccl  15066  vrgpfval  15071  frgpuptinv  15076  frgpup3lem  15082  iscmn  15092  subcmn  15129  frgpnabllem1  15157  iscyg  15162  lt6abl  15177  gsumval3  15187  gsumzf1o  15192  gsum2d  15219  gsumcom2  15222  dmdprd  15232  dprdval  15234  dprd2da  15273  dmdprdsplit2lem  15276  dpjfval  15286  pgpfaclem1  15312  mgpval  15324  mgpplusg  15325  isrng  15341  iscrng  15344  pws1  15395  opprval  15402  crngoppr  15405  dvdsrval  15423  isunit  15435  invrfval  15451  dvrfval  15462  isirred  15477  dfrhm2  15494  pwsco1rhm  15506  pwsco2rhm  15507  isdrng  15512  isdrng2  15518  drngid  15522  isdrngrd  15534  issubrg  15541  abvfval  15579  abvneg  15595  staffval  15608  issrng  15611  issrngd  15622  islmod  15627  scaffval  15641  lssset  15687  prdsvscacl  15721  lspfval  15726  islmhm  15780  islmhm2  15791  islmim  15811  islbs  15825  islvec  15853  2idlval  15981  crng2idl  15987  isnzr  16007  rrgval  16024  isdomn  16031  isassa  16052  aspval  16064  asclfval  16070  psrval  16106  mvrfval  16161  mplval  16169  mplcoe3  16206  mplcoe2  16207  ltbval  16209  opsrval  16212  mplind  16239  vr1cl2  16268  ply1val  16269  psropprmul  16312  coe1mul2lem2  16341  coe1tm  16345  coe1sclmul  16354  coe1sclmul2  16356  ply1scl1  16363  ply1coe  16364  mulgrhm2  16457  zlmval  16466  chrval  16475  znval  16485  znzrhfo  16497  znle2  16503  znunithash  16514  cygznlem1  16516  isphl  16528  phllmhm  16532  ipffval  16548  ocvfval  16562  cssval  16578  cssincl  16584  thlval  16591  pjfval  16602  ishil  16614  isobs  16616  istps  16670  cldval  16756  ntrfval  16757  clsfval  16758  neifval  16832  lpfval  16866  isperf  16878  restbas  16885  tgrest  16886  resstopn  16912  ordtval  16915  ordtuni  16916  ordtbas  16918  ordtrest2  16930  ist0  17044  ist1  17045  ishaus  17046  iscnrm  17047  pnrmopn  17067  iscmp  17111  cmpcld  17125  hauscmplem  17129  cmpfi  17131  iscon  17135  consuba  17142  is1stc  17163  txval  17255  ptval  17261  ptbasin  17268  ptbasfi  17272  xkoval  17278  ptunimpt  17286  ptval2  17292  txbasval  17297  dfac14  17308  upxp  17313  uptx  17315  prdstopn  17318  txrest  17321  ptrescn  17329  lmcn2  17339  xkoptsub  17344  xkopt  17345  xkococn  17350  cnmpt2t  17363  cnmpt2res  17367  cnmpt2k  17378  qtopval  17382  imastopn  17407  hmphindis  17484  ptuncnv  17494  ptunhmeo  17495  xpstopnlem1  17496  xpstopnlem2  17498  xkohmeo  17502  qtophmeo  17504  elmptrab  17518  trfbas2  17534  trfil2  17578  fmco  17652  flimval  17654  flfcnp2  17698  fclsval  17699  fclsrest  17715  alexsublem  17734  alexsubALTlem3  17739  alexsubALTlem4  17740  ptcmplem1  17742  ptcmplem3  17744  ptcmpg  17747  istmd  17753  istgp  17756  istgp2  17770  tgplacthmeo  17782  clssubg  17787  tgpconcompeqg  17790  tsmsval2  17808  istrg  17842  istdrg  17844  istlm  17863  istvc  17870  imasdsf1olem  17933  xpsxmetlem  17939  xpsmet  17942  isxms  17989  isms  17991  tmsval  18023  stdbdxmet  18057  prdsxmslem2  18071  txmetcnp  18089  nmfval  18107  isngp  18114  tngval  18151  tngtopn  18162  tngnm  18163  isnrg  18167  isnlm  18182  nmofval  18219  nghmfval  18227  qtopbaslem  18263  cnblcld  18280  negcncf  18417  negfcncf  18418  cncfcnvcn  18420  cnmptre  18421  cnheiborlem  18448  cnheibor  18449  bndth  18452  pcorev2  18522  om1bas  18525  pi1val  18531  pi1bas3  18537  pi1cpbl  18538  pi1xfrcnv  18551  isclm  18558  nmoleub2lem3  18592  nmoleub3  18596  iscph  18602  cphcjcl  18615  tchval  18646  ipcau2  18660  csscld  18672  iscmet  18706  caubl  18729  caublcls  18730  bcthlem4  18745  bcthlem5  18746  bcth3  18749  isbn  18756  iscms  18763  ovolfioo  18823  ovolficc  18824  ovolficcss  18825  ovolfsval  18826  ovolval  18829  ovollb2lem  18843  ovolctb  18845  ovolunlem1a  18851  ovoliunlem1  18857  ovoliun2  18861  shft2rab  18863  ovolshftlem1  18864  sca2rab  18867  ovolscalem1  18868  ovolicc2lem1  18872  ovolicc2lem4  18875  ovolicc2lem5  18876  cmmbl  18888  unmbl  18891  voliunlem3  18905  iunmbl  18906  voliun  18907  ioombl1lem3  18913  ovolfs2  18922  ioorinv  18927  uniiccdif  18929  uniioovol  18930  uniioombllem2a  18933  uniioombllem2  18934  uniioombllem3a  18935  uniioombllem3  18936  uniioombllem4  18937  uniioombllem5  18938  uniioombllem6  18939  dyadovol  18944  dyadss  18945  dyaddisjlem  18946  dyadmaxlem  18948  dyadmbl  18951  opnmbllem  18952  vitalilem4  18962  ismbf  18981  mbfconst  18986  itg2val  19079  itg2monolem1  19101  itg2i1fseq  19106  dfitg  19120  itgz  19131  itgvallem3  19136  iblcnlem1  19138  iblcnlem  19139  iblposlem  19142  itgreval  19147  itgfsum  19177  bddmulibl  19189  itgcn  19193  limcfval  19218  ellimc  19219  limcmpt2  19230  limccnp  19237  dvfval  19243  eldv  19244  dvreslem  19255  dvres2lem  19256  dvidlem  19261  dvnfval  19267  dvexp2  19299  dvrec  19300  dveflem  19322  dvlipcn  19337  dv11cn  19344  lhop  19359  ftc2  19387  evlsval  19399  evlsval2  19400  evlval  19404  evlrhm  19405  evl1fval  19406  evl1sca  19409  evl1var  19411  pf1subrg  19427  pf1ind  19434  mdegfval  19444  uc1pval  19521  mon1pval  19523  q1pval  19535  r1pval  19538  ig1pval  19554  plyconst  19584  plyeq0lem  19588  dgrval  19606  plyco  19619  0dgrb  19624  coemullem  19627  coe0  19633  coesub  19634  dgrsub  19649  dgrcolem1  19650  dgrcolem2  19651  dgrco  19652  quotval  19668  plydivex  19673  quotlem  19676  plyremlem  19680  fta1  19684  vieta1lem1  19686  vieta1lem2  19687  vieta1  19688  aaliou2  19716  aaliou3lem7  19725  taylpfval  19740  dvtaylp  19745  dvntaylp0  19747  taylthlem1  19748  ulm2  19760  ulmshft  19765  pserdvlem2  19800  abelthlem1  19803  abelthlem8  19811  abelth  19813  abelth2  19814  ptolemy  19860  coskpi  19884  efif1olem2  19901  efif1olem3  19902  logcnlem4  19988  advlogexp  19998  efopn  20001  logtayl  20003  dcubic2  20136  dcubic  20138  quart1lem  20147  atancj  20202  tanatan  20211  cosatan  20213  dvatan  20227  leibpi  20234  birthdaylem2  20243  efrlim  20260  emcllem7  20291  wilthlem2  20303  basellem5  20318  basellem8  20321  basellem9  20322  vmaval  20347  prmorcht  20412  mumul  20415  dvdsmulf1o  20430  fsumdvdsmul  20431  ppiub  20439  fsumvma  20448  pclogsum  20450  dchrval  20469  bposlem8  20526  lgslem1  20531  lgsval  20535  lgsval4  20551  lgsfcl3  20552  lgsdilem  20557  lgsdir2lem4  20561  lgsdir2lem5  20562  lgsquadlem2  20590  dchrisum0flb  20655  rpvmasum2  20657  log2sumbnd  20689  selberglem2  20691  pntibndlem2  20736  pntlemp  20755  ostth2lem3  20780  ostth2lem4  20781  isplig  20838  gidval  20874  grpoinvfval  20885  grpodivfval  20903  gxfval  20918  isablo  20944  subgornss  20967  isexid  20978  elghomlem1  21022  isrngo  21039  drngoi  21068  vci  21098  isvclem  21127  nvop2  21158  nvvop  21159  isnvlem  21160  dipfval  21269  sspval  21293  isssp  21294  lnoval  21324  nmoofval  21334  bloval  21353  0ofval  21359  ajfval  21381  hmoval  21382  isphg  21389  phop  21390  ipasslem11  21412  siii  21425  iscbn  21437  opsqrlem6  22721  elpjrn  22766  hstle1  22802  stm1addi  22821  stm1add3i  22823  mdslmd1lem1  22901  mdexchi  22911  atordi  22960  dmdbr5ati  22998  cdj3lem1  23010  subfacp1lem5  23122  subfacp1lem6  23123  ispcon  23161  pconpi1  23175  rescon  23184  iscvm  23197  cvmsss2  23212  cvmliftlem3  23225  cvmliftlem5  23227  cvmliftlem10  23232  cvmliftlem11  23233  cvmlift2lem9a  23241  cvmlift2lem2  23242  cvmliftphtlem  23255  cvmlift3lem7  23263  umgraex  23282  vdgr1d  23301  eupath2lem3  23310  snmlflim  23322  ghomgrpilem2  23400  fz0n  23503  rdgprc  23555  dfrdg2  23556  dftrpred4g  23641  dfrdg4  23898  colinearalglem4  23947  axlowdimlem3  23982  axlowdimlem16  23995  axlowdimlem17  23996  fvline2  24179  ellines  24185  bpolylem  24193  bpoly1  24196  bpolydiflem  24199  rankeq1o  24211  ordcmp  24296  dvreasin  24333  dvreacos  24334  areacirclem2  24335  areacirclem6  24340  dfoprab4pop  24447  fnovpop  24448  prjdmn  24492  prjrn  24493  mapex2  24551  iscst1  24585  valcurfn1  24615  isorhom  24622  gepsup  24661  seinf  24662  mxlelt  24675  ltrcmp  24816  com2i  24827  idlvalNEW  24856  vri  24903  istopxc  24959  prdnei  24984  limptlimpr2lem2  24986  islimrs  24991  isalg  25132  algi  25138  isded  25147  dedi  25148  dedalg  25154  iscatOLD  25165  cati  25166  catded  25175  ishoma  25198  ismona  25220  isepia  25230  isiso  25236  cinvlem1  25239  isfuna  25245  issubcat  25256  linevala2  25489  isray2  25564  clsun  25657  isfne  25679  isref  25690  isptfin  25706  islocfin  25707  neibastop3  25722  cover2g  25770  f1opr  25802  sdclem1  25864  sstotbnd  25910  ssbnd  25923  prdstotbnd  25929  prdsbnd2  25930  ismtyhmeolem  25939  heiborlem3  25948  heiborlem4  25949  heiborlem6  25951  rrnval  25962  rrncmslem  25967  ismrer1  25973  reheibor  25974  rngohomval  26006  rngoisoval  26019  idlval  26049  pridlval  26069  maxidlval  26075  isprrngo  26086  igenval  26097  fndifnfp  26167  elrfi  26180  isnacs  26190  ofmpteq  26208  diophin  26263  dnnumch1  26552  islmodfg  26578  islnm  26586  lnmlssfg  26589  dsmmval  26611  dsmmbas2  26614  dsmmfi  26615  dsmm0cl  26617  frlmpws  26629  frlmlss  26630  frlmbas  26634  uvcfval  26644  frlmsplit2  26654  mapfien2  26669  frlmpwfi  26673  islindf  26693  lindfmm  26708  islindf5  26720  hbtlem1  26738  hbtlem7  26740  hbtlem6  26744  dgrnznn  26751  pmtrmvd  26809  pmtrfrn  26811  psgnunilem2  26829  psgnfval  26834  psgnghm2  26849  mamufval  26854  matval  26876  matplusg2  26888  matvsca2  26889  mdetfval  26898  mendval  26902  mendplusgfval  26904  mendmulrfval  26906  mendvscafval  26909  fgraphxp  26941  iotain  27028  rfcnpre1  27101  rfcnpre2  27113  rfcnpre3  27115  rfcnpre4  27116  fmuldfeq  27124  itgsinexplem1  27159  stoweidlem34  27194  stoweidlem41  27201  dfafn5a  27413  dfaimafn2  27419  ffnaov  27450  dpval  27512  bnj66  28171  bnj570  28216  bnj1326  28335  bnj1463  28364  bnj1501  28376  lshpset  28447  lsatset  28459  lcvfbr  28489  lflset  28528  lkrfval  28556  lkrval2  28559  ldualset  28594  isopos  28649  cmtfvalN  28679  isoml  28707  cvrfval  28737  pats  28754  isatl  28768  iscvlat  28792  ishlat1  28821  llnset  28973  lplnset  28997  lvolset  29040  dalem58  29198  dalem59  29199  lineset  29206  pointsetN  29209  psubspset  29212  pmapfval  29224  paddfval  29265  pclfvalN  29357  polfvalN  29372  psubclsetN  29404  watfvalN  29460  lhpset  29463  lautset  29550  pautsetN  29566  ldilfset  29576  ltrnfset  29585  ltrnset  29586  ltrncoidN  29596  dilfsetN  29620  trnfsetN  29623  trlfset  29628  trlset  29629  cdleme6  29709  cdleme11g  29733  cdleme31sn1  29849  cdleme31sn1c  29856  cdleme31sn2  29857  cdleme40v  29937  cdleme42ke  29953  cdleme50trn2a  30018  cdleme50trn3  30021  cdlemg1b2  30039  cdlemg47  30204  tgrpfset  30212  tgrpset  30213  tendofset  30226  tendoset  30227  erngfset  30267  erngset  30268  erngfset-rN  30275  erngset-rN  30276  cdlemi  30288  cdlemk4  30302  cdlemkuu  30363  cdlemk35  30380  cdlemky  30394  cdlemk54  30426  cdlemk55a  30427  cdlemkyyN  30430  dva1dim  30453  erngdvlem3-rN  30466  dvafset  30472  dvaset  30473  diaffval  30499  diafval  30500  diaintclN  30527  dvhfset  30549  dvhset  30550  cdlemm10N  30587  docaffvalN  30590  docafvalN  30591  djaffvalN  30602  djafvalN  30603  dibffval  30609  dibfval  30610  dib1dim  30634  dibintclN  30636  dicffval  30643  dicfval  30644  dicval2  30648  dihffval  30699  dihfval  30700  dihopelvalcpre  30717  dihmeetbclemN  30773  dih1dimatlem  30798  dihglb2  30811  dihintcl  30813  dochffval  30818  dochfval  30819  djhffval  30865  djhfval  30866  dihjatcclem1  30887  dihjatcclem3  30889  djhlsmat  30896  lpolsetN  30951  lcdfval  31057  lcdval  31058  lcdval2  31059  lcdsca  31068  mapdffval  31095  mapdfval  31096  mapdval3N  31100  mapdval5N  31102  mapdpglem21  31161  hvmapffval  31227  hvmapfval  31228  hdmap1ffval  31265  hdmap1fval  31266  hdmapffval  31298  hdmapfval  31299  hgmapffval  31357  hgmapfval  31358  hdmapoc  31403  hlhilset  31406  hlhilslem  31410  hlhilnvl  31422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-cleq 2277
  Copyright terms: Public domain W3C validator