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

Theorem syl6eqr 2416
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 2370 . 2  |-  B  =  C
41, 3syl6eq 2414 1  |-  ( ph  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1647
This theorem is referenced by:  3eqtr4g  2423  iinrab2  4067  relop  4937  dfiun3g  5034  dfiin3g  5035  resima2  5091  relcnvfld  5306  uniabio  5332  iotanul  5337  fntpg  5410  dffn5  5675  dfimafn2  5679  fncnvima2  5754  fmptcof  5803  fcoconst  5806  fnpr  5850  fnprOLD  5851  resfunexg  5857  ffnov  6074  fnov  6078  fnrnov  6119  foov  6120  funimassov  6123  ovelimab  6124  ofc12  6229  caofinvl  6231  1st2val  6272  2nd2val  6273  curry1  6338  curry2  6341  dftpos3  6394  riotav  6451  riotauni  6453  tz7.44-3  6563  rdgsucmptnf  6584  rdglim2a  6588  frsucmptn  6593  seqomlem1  6604  seqomlem4  6607  oa0r  6679  om1r  6683  oarec  6702  oacomf1olem  6704  oeeulem  6741  omabs  6787  ecinxp  6876  mapunen  7173  phplem1  7183  fodomfi  7282  iinfi  7318  fiin  7322  dffi3  7331  ordtypelem3  7382  ordtypelem9  7388  cantnffval  7511  cantnfval  7516  cantnfp1lem3  7529  cantnflem1  7538  wemapwe  7547  oef1o  7548  cnfcom2lem  7551  rankuni  7682  cardval2  7771  dfac8alem  7803  dfac12lem1  7916  cda1dif  7949  cdaassen  7955  isf34lem4  8150  hsmexlem5  8203  axdc3lem4  8226  axdc4lem  8228  ac6num  8253  zorn2lem1  8270  ttukeylem3  8285  pwcfsdom  8352  fpwwe2lem9  8407  canth4  8416  canthp1lem2  8422  genpass  8780  prlem934  8804  mulcmpblnrlem  8842  recexsrlem  8872  supsrlem  8880  axrnegex  8931  nneo  10246  cnref1o  10500  xmulneg1  10741  xmulpnf1n  10750  xadddi  10767  fztp  10994  fseq1m1p1  11013  uzrdgsuci  11187  seqof2  11268  mulexpz  11307  expaddz  11311  bcp1m1  11498  hash1snb  11568  seqcoll  11599  iswrdi  11618  cjexp  11842  rexuz3  12039  limsupval  12155  limsupgle  12158  climconst  12224  zsum  12399  fsum  12401  sum0  12402  sumz  12403  fsumcnv  12444  incexc2  12505  mertenslem2  12549  efval2  12573  ege2le3  12579  efzval  12590  efival  12640  sinbnd  12668  cosbnd  12669  sadfval  12851  bitsres  12872  smufval  12876  smupp1  12879  eucalgval  12960  eucalginv  12962  eucalglt  12963  eucalgcvga  12964  eucalg  12965  dfphi2  13050  phimullem  13055  prmdiv  13061  odzval  13064  pcval  13105  pczpre  13108  pcrec  13119  prmreclem6  13176  4sqlem17  13216  vdwmc  13233  vdwpc  13235  vdwlem8  13243  ramval  13263  ramcl  13284  ressval  13403  resslem  13409  firest  13547  topnval  13549  prdsval  13565  prdsleval  13586  prdsbas3  13590  prdsdsval2  13593  pwsval  13595  pwsbas  13596  pwselbasb  13597  pwsplusgval  13599  pwsmulrval  13600  pwsle  13601  pwsvscafval  13603  imasval  13624  imasdsval  13628  imasdsval2  13629  divsval  13654  xpsval  13684  xpslem  13685  xpsaddlem  13687  xpsvsca  13691  xpsle  13693  mrisval  13742  iscat  13784  cidfval  13788  homffval  13804  comfffval  13811  comffval  13812  comfeq  13819  oppcval  13826  oppchomfval  13827  oppccofval  13829  oppcbas  13831  oppcid  13834  monfval  13845  oppcmon  13851  sectffval  13863  invffval  13870  isoval  13877  isssc  13907  rescbas  13916  reschomf  13918  issubc  13922  isfunc  13948  isfuncd  13949  funcf2  13952  idfuval  13960  idfu2nd  13961  cofucl  13972  resfval2  13977  resf2nd  13979  funcres2b  13981  funcpropd  13984  isfull  13994  isfth  13998  natfval  14030  fucval  14042  fuccofval  14043  fucbas  14044  fuchom  14045  homafval  14071  homaval  14073  homadmcd  14084  arwval  14085  arwhoma  14087  idafval  14099  coafval  14106  coapm  14113  catcco  14143  catcid  14145  catcisolem  14148  xpcval  14161  xpcco  14167  1stfval  14175  2ndfval  14178  xpcpropd  14192  evlfval  14201  evlfcllem  14205  evlfcl  14206  curfval  14207  curf1cl  14212  curfcl  14216  uncf1  14220  uncf2  14221  uncfcurf  14223  diag2  14229  curf2ndf  14231  hofval  14236  hof2fval  14239  hofcl  14243  yonval  14245  hofpropd  14251  yonedalem21  14257  yonedalem22  14262  yonedalem3  14264  yonedainv  14265  yonffthlem  14266  isdrs  14278  ispos  14291  pltfval  14303  lubfval  14322  glbfval  14327  joinfval  14331  meetfval  14338  p0val  14357  p1val  14358  islat  14363  isclat  14425  ipoval  14467  isipodrs  14474  isdlat  14506  istsr  14536  spwval2  14543  isla  14552  isdir  14564  ismnd  14579  plusffval  14589  grpidval  14594  ismgmid  14597  pws0g  14618  ismhm  14627  submacs  14652  gsumvalx  14661  frmdval  14683  isgrp  14703  grpn0  14724  grpinvfval  14730  grpsubfval  14734  mulgfval  14778  mulgval  14779  mulgnn0p1  14788  pwsinvg  14817  issubg  14831  isnsg  14856  eqgfval  14875  divseccl  14883  isghm  14893  conjsubg  14924  conjsubgen  14925  isgim  14936  isga  14955  symgval  14981  cntrval  15005  cntzfval  15006  oppgval  15030  invoppggim  15043  odfval  15058  odval  15059  gexval  15099  ispgp  15113  sylow1lem1  15119  slwispgp  15132  pgpssslw  15135  sylow2alem2  15139  sylow3lem5  15152  lsmfval  15159  pj1fval  15213  efgmnvl  15233  efgval  15236  efgval2  15243  efginvrel2  15246  efgsfo  15258  efgredleme  15262  efgredlemd  15263  efgredlemc  15264  frgpval  15277  frgpeccl  15280  vrgpfval  15285  frgpuptinv  15290  frgpup3lem  15296  iscmn  15306  subcmn  15343  frgpnabllem1  15371  iscyg  15376  lt6abl  15391  gsumval3  15401  gsumzf1o  15406  gsum2d  15433  gsumcom2  15436  dmdprd  15446  dprdval  15448  dprd2da  15487  dmdprdsplit2lem  15490  dpjfval  15500  pgpfaclem1  15526  mgpval  15538  mgpplusg  15539  isrng  15555  iscrng  15558  pws1  15609  opprval  15616  crngoppr  15619  dvdsrval  15637  isunit  15649  invrfval  15665  dvrfval  15676  isirred  15691  dfrhm2  15708  pwsco1rhm  15720  pwsco2rhm  15721  isdrng  15726  isdrng2  15732  drngid  15736  isdrngrd  15748  issubrg  15755  abvfval  15793  abvneg  15809  staffval  15822  issrng  15825  issrngd  15836  islmod  15841  scaffval  15855  lssset  15901  prdsvscacl  15935  lspfval  15940  islmhm  15994  islmhm2  16005  islmim  16025  islbs  16039  islvec  16067  2idlval  16195  crng2idl  16201  isnzr  16221  rrgval  16238  isdomn  16245  isassa  16266  aspval  16278  asclfval  16284  psrval  16320  mvrfval  16375  mplval  16383  mplcoe3  16420  mplcoe2  16421  ltbval  16423  opsrval  16426  mplind  16453  vr1cl2  16482  ply1val  16483  psropprmul  16526  coe1mul2lem2  16555  coe1tm  16559  coe1sclmul  16568  coe1sclmul2  16570  ply1scl1  16577  ply1coe  16578  mulgrhm2  16678  zlmval  16687  chrval  16696  znval  16706  znzrhfo  16718  znle2  16724  znunithash  16735  cygznlem1  16737  isphl  16749  phllmhm  16753  ipffval  16769  ocvfval  16783  cssval  16799  cssincl  16805  thlval  16812  pjfval  16823  ishil  16835  isobs  16837  istps  16891  cldval  16977  ntrfval  16978  clsfval  16979  neifval  17053  lpfval  17087  isperf  17099  restbas  17106  tgrest  17107  resstopn  17133  ordtval  17136  ordtuni  17137  ordtbas  17139  ordtrest2  17151  ist0  17265  ist1  17266  ishaus  17267  iscnrm  17268  pnrmopn  17288  iscmp  17332  cmpcld  17346  hauscmplem  17350  cmpfi  17352  iscon  17356  consuba  17363  is1stc  17384  txval  17476  ptval  17482  ptbasin  17489  ptbasfi  17493  xkoval  17499  ptunimpt  17507  ptval2  17513  txbasval  17518  dfac14  17529  upxp  17534  uptx  17536  prdstopn  17539  txrest  17542  ptrescn  17550  lmcn2  17560  xkoptsub  17565  xkopt  17566  xkococn  17571  cnmpt2t  17584  cnmpt2res  17588  cnmpt2k  17599  qtopval  17603  imastopn  17628  hmphindis  17705  ptuncnv  17715  ptunhmeo  17716  xpstopnlem1  17717  xpstopnlem2  17719  xkohmeo  17723  qtophmeo  17725  elmptrab  17735  trfbas2  17751  trfil2  17795  fmco  17869  flimval  17871  flfcnp2  17915  fclsval  17916  fclsrest  17932  alexsublem  17951  alexsubALTlem3  17956  alexsubALTlem4  17957  ptcmplem1  17959  ptcmplem3  17961  ptcmpg  17964  istmd  17970  istgp  17973  istgp2  17987  tgplacthmeo  17999  clssubg  18004  tgpconcompeqg  18007  tsmsval2  18025  istrg  18059  istdrg  18061  istlm  18080  istvc  18087  imasdsf1olem  18150  xpsxmetlem  18156  xpsmet  18159  isxms  18206  isms  18208  tmsval  18240  stdbdxmet  18274  prdsxmslem2  18288  txmetcnp  18306  nmfval  18324  isngp  18331  tngval  18368  tngtopn  18379  tngnm  18380  isnrg  18384  isnlm  18399  nmofval  18436  nghmfval  18444  qtopbaslem  18480  cnblcld  18497  negcncf  18636  negfcncf  18637  cncfcnvcn  18639  cnmptre  18640  cnheiborlem  18667  cnheibor  18668  bndth  18671  pcorev2  18741  om1bas  18744  pi1val  18750  pi1bas3  18756  pi1cpbl  18757  pi1xfrcnv  18770  isclm  18777  nmoleub2lem3  18811  nmoleub3  18815  iscph  18821  cphcjcl  18834  tchval  18865  ipcau2  18879  csscld  18891  iscmet  18925  caubl  18948  caublcls  18949  bcthlem4  18964  bcthlem5  18965  bcth3  18968  isbn  18975  iscms  18982  ovolfioo  19042  ovolficc  19043  ovolficcss  19044  ovolfsval  19045  ovolval  19048  ovollb2lem  19062  ovolctb  19064  ovolunlem1a  19070  ovoliunlem1  19076  ovoliun2  19080  shft2rab  19082  ovolshftlem1  19083  sca2rab  19086  ovolscalem1  19087  ovolicc2lem1  19091  ovolicc2lem4  19094  ovolicc2lem5  19095  cmmbl  19107  unmbl  19110  voliunlem3  19124  iunmbl  19125  voliun  19126  ioombl1lem3  19132  ovolfs2  19141  ioorinv  19146  uniiccdif  19148  uniioovol  19149  uniioombllem2a  19152  uniioombllem2  19153  uniioombllem3a  19154  uniioombllem3  19155  uniioombllem4  19156  uniioombllem5  19157  uniioombllem6  19158  dyadovol  19163  dyadss  19164  dyaddisjlem  19165  dyadmaxlem  19167  dyadmbl  19170  opnmbllem  19171  vitalilem4  19181  ismbf  19200  mbfconst  19205  itg2val  19298  itg2monolem1  19320  itg2i1fseq  19325  dfitg  19339  itgz  19350  itgvallem3  19355  iblcnlem1  19357  iblcnlem  19358  iblposlem  19361  itgreval  19366  itgfsum  19396  bddmulibl  19408  itgcn  19412  limcfval  19437  ellimc  19438  limcmpt2  19449  limccnp  19456  dvfval  19462  eldv  19463  dvreslem  19474  dvres2lem  19475  dvidlem  19480  dvnfval  19486  dvexp2  19518  dvrec  19519  dveflem  19541  dvlipcn  19556  dv11cn  19563  lhop  19578  ftc2  19606  evlsval  19618  evlsval2  19619  evlval  19623  evlrhm  19624  evl1fval  19625  evl1sca  19628  evl1var  19630  pf1subrg  19646  pf1ind  19653  mdegfval  19663  uc1pval  19740  mon1pval  19742  q1pval  19754  r1pval  19757  ig1pval  19773  plyconst  19803  plyeq0lem  19807  dgrval  19825  plyco  19838  0dgrb  19843  coemullem  19846  coe0  19852  coesub  19853  dgrsub  19868  dgrcolem1  19869  dgrcolem2  19870  dgrco  19871  quotval  19887  plydivex  19892  quotlem  19895  plyremlem  19899  fta1  19903  vieta1lem1  19905  vieta1lem2  19906  vieta1  19907  aaliou2  19935  aaliou3lem7  19944  taylpfval  19959  dvtaylp  19964  dvntaylp0  19966  taylthlem1  19967  ulm2  19979  ulmshft  19984  pserdvlem2  20022  abelthlem1  20025  abelthlem8  20033  abelth  20035  abelth2  20036  ptolemy  20082  coskpi  20106  efif1olem2  20123  efif1olem3  20124  logcnlem4  20214  advlogexp  20224  efopn  20227  logtayl  20229  dcubic2  20362  dcubic  20364  quart1lem  20373  atancj  20428  tanatan  20437  cosatan  20439  dvatan  20453  leibpi  20460  birthdaylem2  20469  efrlim  20486  emcllem7  20518  wilthlem2  20530  basellem5  20545  basellem8  20548  basellem9  20549  vmaval  20574  prmorcht  20639  mumul  20642  dvdsmulf1o  20657  fsumdvdsmul  20658  ppiub  20666  fsumvma  20675  pclogsum  20677  dchrval  20696  bposlem8  20753  lgslem1  20758  lgsval  20762  lgsval4  20778  lgsfcl3  20779  lgsdilem  20784  lgsdir2lem4  20788  lgsdir2lem5  20789  lgsquadlem2  20817  dchrisum0flb  20882  rpvmasum2  20884  log2sumbnd  20916  selberglem2  20918  pntibndlem2  20963  pntlemp  20982  ostth2lem3  21007  ostth2lem4  21008  umgraex  21036  nbgraf1olem5  21125  vdgr1d  21186  eupath2lem3  21212  isplig  21276  gidval  21312  grpoinvfval  21323  grpodivfval  21341  gxfval  21356  isablo  21382  subgornss  21405  isexid  21416  elghomlem1  21460  isrngo  21477  drngoi  21506  vci  21538  isvclem  21567  nvop2  21598  nvvop  21599  isnvlem  21600  dipfval  21709  sspval  21733  isssp  21734  lnoval  21764  nmoofval  21774  bloval  21793  0ofval  21799  ajfval  21821  hmoval  21822  isphg  21829  phop  21830  ipasslem11  21852  siii  21865  iscbn  21877  opsqrlem6  23159  elpjrn  23204  hstle1  23240  stm1addi  23259  stm1add3i  23261  mdslmd1lem1  23339  mdexchi  23349  atordi  23398  dmdbr5ati  23436  cdj3lem1  23448  disjabrex  23543  disjabrexf  23544  feqmptdf  23599  xrofsup  23647  xpinpreima2  23781  xrge0mulc1cn  23803  ustbas  23851  trust  23853  ustuqtop1  23865  ustuqtop2  23866  utopsnneiplem  23871  isusp  23880  zlmds  23943  qqhval  23951  rrhval  23971  esumsn  24042  ofcc  24075  sxval  24130  measvuni  24152  volmeas  24171  elunirnmbfm  24187  totprob  24254  orrvcval4  24291  lgamcvglem  24393  subfacp1lem5  24439  subfacp1lem6  24440  ispcon  24478  pconpi1  24492  rescon  24501  iscvm  24514  cvmsss2  24529  cvmliftlem3  24542  cvmliftlem5  24544  cvmliftlem10  24549  cvmliftlem11  24550  cvmlift2lem9a  24558  cvmlift2lem2  24559  cvmliftphtlem  24572  cvmlift3lem7  24580  snmlflim  24587  ghomgrpilem2  24665  fz0n  24771  zprod  24832  fprod  24836  prod0  24838  prod1  24839  rdgprc  24977  dfrdg2  24978  dftrpred4g  25063  dfrdg4  25315  colinearalglem4  25364  axlowdimlem3  25399  axlowdimlem16  25412  axlowdimlem17  25413  fvline2  25596  ellines  25602  bpolylem  25610  bpoly1  25613  bpolydiflem  25616  rankeq1o  25628  ordcmp  25713  volsupnfl  25759  itg2addnclem  25760  itgaddnclem2  25767  dvreasin  25783  dvreacos  25784  areacirclem2  25785  areacirclem6  25790  clsun  25838  isfne  25860  isref  25871  isptfin  25887  islocfin  25888  neibastop3  25903  cover2g  25951  f1opr  25983  sdclem1  26045  sstotbnd  26090  ssbnd  26103  prdstotbnd  26109  prdsbnd2  26110  ismtyhmeolem  26119  heiborlem3  26128  heiborlem4  26129  heiborlem6  26131  rrnval  26142  rrncmslem  26147  ismrer1  26153  reheibor  26154  rngohomval  26186  rngoisoval  26199  idlval  26229  pridlval  26249  maxidlval  26255  isprrngo  26266  igenval  26277  fndifnfp  26347  elrfi  26360  isnacs  26370  ofmpteq  26388  diophin  26443  dnnumch1  26732  islmodfg  26758  islnm  26766  lnmlssfg  26769  dsmmval  26791  dsmmbas2  26794  dsmmfi  26795  dsmm0cl  26797  frlmpws  26809  frlmlss  26810  frlmbas  26814  uvcfval  26824  frlmsplit2  26834  mapfien2  26849  frlmpwfi  26853  islindf  26873  lindfmm  26888  islindf5  26900  hbtlem1  26918  hbtlem7  26920  hbtlem6  26924  dgrnznn  26931  pmtrmvd  26989  pmtrfrn  26991  psgnunilem2  27009  psgnfval  27014  psgnghm2  27029  mamufval  27034  matval  27056  matplusg2  27068  matvsca2  27069  mdetfval  27078  mendval  27082  mendplusgfval  27084  mendmulrfval  27086  mendvscafval  27089  fgraphxp  27121  iotain  27208  rfcnpre1  27281  rfcnpre2  27293  rfcnpre3  27295  rfcnpre4  27296  fmuldfeq  27304  itgsinexplem1  27339  stoweidlem34  27374  stoweidlem41  27381  dfafn5a  27616  dfaimafn2  27622  ffnaov  27655  usgraexvlem  27664  constr3trllem3  27787  constr3cycllem1  27793  1to2vfriswmgra  27830  dpval  27930  bnj66  28644  bnj570  28689  bnj1326  28808  bnj1463  28837  bnj1501  28849  lshpset  29227  lsatset  29239  lcvfbr  29269  lflset  29308  lkrfval  29336  lkrval2  29339  ldualset  29374  isopos  29429  cmtfvalN  29459  isoml  29487  cvrfval  29517  pats  29534  isatl  29548  iscvlat  29572  ishlat1  29601  llnset  29753  lplnset  29777  lvolset  29820  dalem58  29978  dalem59  29979  lineset  29986  pointsetN  29989  psubspset  29992  pmapfval  30004  paddfval  30045  pclfvalN  30137  polfvalN  30152  psubclsetN  30184  watfvalN  30240  lhpset  30243  lautset  30330  pautsetN  30346  ldilfset  30356  ltrnfset  30365  ltrnset  30366  ltrncoidN  30376  dilfsetN  30400  trnfsetN  30403  trlfset  30408  trlset  30409  cdleme6  30489  cdleme11g  30513  cdleme31sn1  30629  cdleme31sn1c  30636  cdleme31sn2  30637  cdleme40v  30717  cdleme42ke  30733  cdleme50trn2a  30798  cdleme50trn3  30801  cdlemg1b2  30819  cdlemg47  30984  tgrpfset  30992  tgrpset  30993  tendofset  31006  tendoset  31007  erngfset  31047  erngset  31048  erngfset-rN  31055  erngset-rN  31056  cdlemi  31068  cdlemk4  31082  cdlemkuu  31143  cdlemk35  31160  cdlemky  31174  cdlemk54  31206  cdlemk55a  31207  cdlemkyyN  31210  dva1dim  31233  erngdvlem3-rN  31246  dvafset  31252  dvaset  31253  diaffval  31279  diafval  31280  diaintclN  31307  dvhfset  31329  dvhset  31330  cdlemm10N  31367  docaffvalN  31370  docafvalN  31371  djaffvalN  31382  djafvalN  31383  dibffval  31389  dibfval  31390  dib1dim  31414  dibintclN  31416  dicffval  31423  dicfval  31424  dicval2  31428  dihffval  31479  dihfval  31480  dihopelvalcpre  31497  dihmeetbclemN  31553  dih1dimatlem  31578  dihglb2  31591  dihintcl  31593  dochffval  31598  dochfval  31599  djhffval  31645  djhfval  31646  dihjatcclem1  31667  dihjatcclem3  31669  djhlsmat  31676  lpolsetN  31731  lcdfval  31837  lcdval  31838  lcdval2  31839  lcdsca  31848  mapdffval  31875  mapdfval  31876  mapdval3N  31880  mapdval5N  31882  mapdpglem21  31941  hvmapffval  32007  hvmapfval  32008  hdmap1ffval  32045  hdmap1fval  32046  hdmapffval  32078  hdmapfval  32079  hgmapffval  32137  hgmapfval  32138  hdmapoc  32183  hlhilset  32186  hlhilslem  32190  hlhilnvl  32202
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-ex 1547  df-cleq 2359
  Copyright terms: Public domain W3C validator