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

Theorem syl5eqel 2543
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eqel.1  |-  A  =  B
syl5eqel.2  |-  ( ph  ->  B  e.  C )
Assertion
Ref Expression
syl5eqel  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl5eqel
StepHypRef Expression
1 syl5eqel.1 . . 3  |-  A  =  B
21a1i 11 . 2  |-  ( ph  ->  A  =  B )
3 syl5eqel.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3eqeltrd 2539 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2443  df-clel 2446
This theorem is referenced by:  syl5eqelr  2544  3eltr4g  2557  csbexg  4522  csbexgOLD  4524  rabexd  4542  snex  4631  dmresexg  5231  riotaprop  6175  fovrn  6333  fnovrn  6338  ovima0  6342  f1oabexg  6636  cofunexg  6641  cofunex2g  6642  abrexex2g  6654  xpexgALT  6670  opiota  6733  fnwelem  6787  mptsuppdifd  6811  fvmpt2curryd  6890  tfrlem12  6948  rdgseg  6978  oelim2  7134  oeeulem  7140  ecexg  7205  qsexg  7258  pmex  7319  resixpfo  7401  elixpsn  7402  unxpdomlem3  7620  rabfi  7638  fnfi  7690  rnfi  7697  iunfi  7700  unifi  7701  pwfilem  7706  fsuppun  7740  fsuppcolem  7751  mapfienlem2  7756  supexd  7804  cantnfp1lem1  7987  oemapvali  7993  mapfienOLD  8028  wemapwe  8029  wemapweOLD  8030  cnfcomlem  8033  cnfcom  8034  cnfcom2lem  8035  cnfcom2  8036  cnfcom3lem  8037  cnfcom3  8038  cnfcomlemOLD  8041  cnfcomOLD  8042  cnfcom2lemOLD  8043  cnfcom2OLD  8044  cnfcom3lemOLD  8045  cnfcom3OLD  8046  prwf  8119  scott0  8194  htalem  8204  infxpenlem  8281  dfac8b  8302  cfss  8535  cofsmo  8539  coftr  8543  fin1a2lem10  8679  hsmexlem4  8699  hsmex2  8703  fpwwe  8914  canthwelem  8918  pwfseqlem1  8926  wuntp  8979  wunsn  8984  wunsuc  8985  wunr1om  8987  wunot  8991  r1limwun  9004  tsk1  9032  tsk2  9033  tskr1om  9035  gruuni  9068  grusn  9072  gruina  9086  wuncn  9438  negcl  9711  peano5nni  10426  peano5uzi  10831  quoremz  11795  quoremnn0  11796  quoremnn0ALT  11797  intfrac2  11798  intfracq  11799  seqf1olem1  11946  seqf1olem2  11947  serle  11962  discr1  12101  swrdccatin2  12480  swrdccatin12lem2  12482  swrdccatin12  12484  swrdccat3  12485  swrdccat3a  12487  cats1cld  12584  sqrlem4  12837  sqreulem  12949  reccn2  13176  fsump1i  13338  fsumabs  13366  o1fsum  13378  supcvg  13420  mertenslem1  13446  mertenslem2  13447  rpnnen2  13610  ruclem12  13625  bitsfzolem  13732  bezoutlem2  13825  algrf  13850  algcvg  13853  algcvga  13856  algfx  13857  eucalgcvga  13863  eucalg  13864  prmdiv  13962  pythagtriplem11  13994  pythagtriplem13  13996  pcprecl  14008  infpnlem1  14073  infpnlem2  14074  4sqlem5  14105  mul4sqlem  14116  4sqlem13  14120  4sqlem14  14121  4sqlem17  14124  4sqlem18  14125  vdwlem5  14148  wunndx  14292  wunress  14339  restid  14474  mreexdomd  14689  acsfn0  14700  acsfn1  14701  acsfn2  14703  funcf2  14880  funcpropd  14912  fthepi  14940  ressffth  14950  elhomai2  15004  catcxpccl  15119  diag1cl  15154  yonedalem1  15184  prdsinvlem  15765  subggrp  15786  nsgacs  15819  ghmima  15869  gimco  15898  gicref  15901  cntrnsg  15961  oppgmnd  15971  cayley  16021  symgfixfolem1  16046  pmtrdifellem1  16084  psgndmsubg  16110  efgredlemf  16342  efgredlemd  16345  efgredlemc  16346  cycsubgcyg  16481  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsum2dlem1  16566  gsum2dlem2  16567  gsum2dOLD  16569  dprdfid  16612  dprdfidOLD  16619  dprd2dlem1  16645  dprd2da  16646  ablfacrplem  16671  ablfacrp  16672  ablfacrp2  16673  ablfac1lem  16674  pgpfac1lem1  16680  pgpfac1lem2  16681  pgpfac1lem3a  16682  pgpfac1lem3  16683  pgpfac1lem4  16684  pgpfac1lem5  16685  pgpfaclem1  16687  ablfaclem3  16693  opprrng  16829  subrgrng  16974  lmhmkerlss  17238  rlmlmod  17392  lidl0cl  17400  lidlacl  17401  lidlnegcl  17402  lidlmcl  17405  lidlacs  17409  fidomndrnglem  17484  gsumbagdiag  17552  psrass1lem  17553  psrlidm  17580  psrridm  17582  mplsubrglem  17624  mplsubrglemOLD  17625  vr1cl2  17756  vr1cl  17778  subrgvr1cl  17823  evl1rhm  17875  evl1gsumdlem  17899  zringlpirlem2  18013  zringlpirlem3  18014  zlpirlem2  18018  zlpirlem3  18019  cygznlem1  18108  cygznlem2a  18109  cygznlem3  18111  isphld  18192  lindsmm  18366  1marepvmarrepid  18497  1marepvsma1  18505  mdetleib2  18510  smadiadetlem3  18590  cramerimplem1  18605  cramerimplem2  18606  cramerimplem3  18607  cramerimp  18608  topopn  18635  rintopn  18638  fctop  18724  topcld  18755  intcld  18760  uncld  18761  unicld  18766  mretopd  18812  neiptoptop  18851  tgrest  18879  restin  18886  neitr  18900  restcls  18901  restntr  18902  restlp  18903  restperf  18904  perfopn  18905  ordtbaslem  18908  ordtuni  18910  ordtbas2  18911  ordtbas  18912  ordttopon  18913  ordtopn1  18914  ordtopn2  18915  ordtrest2lem  18923  ordtrest2  18924  cnco  18986  cnrest  19005  cnprest2  19010  lmss  19018  cncmp  19111  imacmp  19116  fiuncmp  19123  bwthOLD  19130  concompcon  19152  cldllycmp  19215  hausmapdom  19220  kgentopon  19227  1stckgen  19243  ptbasin  19266  ptbasfi  19270  pttopon  19285  xkotopon  19289  txbasval  19295  ptpjcn  19300  ptcldmpt  19303  dfac14lem  19306  txcn  19315  ptcn  19316  ptrescn  19328  txkgen  19341  cnmpt12f  19355  xkofvcn  19373  qtopval2  19385  elqtop  19386  qtoptop2  19388  hmeoco  19461  idhmeo  19462  ordthmeolem  19490  ptunhmeo  19497  xkohmeo  19504  qtopf1  19505  cfinfil  19582  ufprim  19598  ufildr  19620  fin1aufil  19621  fmfg  19638  elfm3  19639  fbflim  19665  flimclslem  19673  flffbas  19684  cnpflf2  19689  flfcnp2  19696  fclsbas  19710  alexsublem  19732  ptcmplem3  19742  ptcmpg  19745  cnextcn  19755  tgpsubcn  19777  tmdgsum  19782  symgtgp  19788  tmdlactcn  19789  submtmd  19791  clssubg  19795  divstgplem  19807  prdstmdd  19810  tsmsfbas  19814  eltsms  19819  tsmssubm  19832  dvrcn  19874  utop2nei  19941  utop3cls  19942  utopreg  19943  blres  20122  prdsbl  20182  metrest  20215  metustexhalfOLD  20254  metustexhalf  20255  subgngp  20337  nlmvscnlem2  20382  nlmvscnlem1  20383  nrginvrcnlem  20387  qtopbaslem  20453  tgqioo  20493  icccmplem2  20516  icccmp  20518  reconnlem2  20520  xrge0tsms  20527  nmcn  20537  metnrmlem2  20552  divcn  20560  fsumcn  20562  fsum2cn  20563  cncfmet  20600  addccncf  20608  cnmpt2pc  20616  icchmeo  20629  cnrehmeo  20641  cnheiborlem  20642  bndth  20646  lebnumlem2  20650  htpycom  20664  htpyid  20665  htpyco1  20666  htpycc  20668  reparphti  20685  pcohtpylem  20707  pcoptcl  20709  pcoass  20712  pcorevcl  20713  pcorevlem  20714  ipcnlem2  20872  ipcnlem1  20873  cmsss  20977  minveclem4c  21028  minveclem3b  21031  minveclem4a  21033  minveclem4  21035  minveclem6  21037  pjthlem1  21040  ivthlem2  21052  ivthlem3  21053  ovolicc2lem4  21119  finiunmbl  21141  voliunlem1  21147  ioombl1lem1  21155  ioombl1lem3  21157  ioombl1lem4  21158  ovolioo  21165  opnmblALT  21199  mbfimaicc  21227  mbfid  21230  mbfeqalem  21236  mbfres  21238  cncombf  21252  mbfi1flim  21317  itg2monolem2  21345  itg2monolem3  21346  itg2mono  21347  itg2cnlem1  21355  itgcl  21377  iblss  21398  itgeqa  21407  itgss3  21408  itgless  21410  iblconst  21411  ibladdlem  21413  itgaddlem1  21416  iblabslem  21421  iblabsr  21423  iblmulc2  21424  itggt0  21435  itgcn  21436  limcvallem  21462  limcflflem  21471  limcres  21477  cnplimc  21478  limccnp  21482  limccnp2  21483  dvreslem  21500  dvres2lem  21501  dvcnp  21509  dvnff  21513  dvmptres2  21552  dvmptres  21553  dvmptntr  21561  dvmptfsum  21563  dvcnvlem  21564  dvcnv  21565  dvferm1lem  21572  dvferm2lem  21574  dvlipcn  21582  dvlip2  21583  c1liplem1  21584  lhop1lem  21601  dvcnvrelem2  21606  dvcvx  21608  dvfsumge  21610  dvfsumlem3  21616  ftc1lem3  21626  ftc1lem4  21627  mdegleb  21651  ply1remlem  21750  ply0  21792  plyid  21793  plyeq0lem  21794  dgrub  21818  dgrub2  21819  dgrlb  21820  coeidlem  21821  coeaddlem  21832  coemullem  21833  coemulhi  21837  dgreq0  21848  dgrlt  21849  dgradd2  21851  dgrmul  21853  dgrcolem2  21857  dgrco  21858  plycj  21860  coecj  21861  plydivlem2  21876  plydivlem4  21878  plyremlem  21886  plyrem  21887  quotcan  21891  vieta1lem1  21892  elqaalem2  21902  elqaalem3  21903  radcnvcl  21998  psercnlem1  22006  pserdvlem2  22009  pilem2  22033  pilem3  22034  logfac  22165  logcnlem2  22204  logcnlem3  22205  logcnlem4  22206  dvlog  22212  cxpcn  22299  cxpcn3lem  22301  ang180lem1  22321  ang180lem2  22322  ang180lem3  22323  pythag  22329  heron  22349  quart1lem  22366  xrlimcnp  22478  efrlim  22479  ftalem1  22526  ftalem2  22527  ftalem4  22529  ftalem5  22530  basellem1  22534  basellem2  22535  basellem3  22536  basellem4  22537  basellem5  22538  basellem8  22541  dchr1cl  22706  dchrinvcl  22708  dchrptlem1  22719  dchrptlem2  22720  bposlem3  22741  bposlem5  22743  bposlem6  22744  lgsqrlem2  22797  lgsqrlem3  22798  lgsqrlem4  22799  lgseisenlem1  22804  lgseisenlem2  22805  lgseisenlem3  22806  lgseisenlem4  22807  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  2sqlem8  22827  chebbnd1lem1  22834  chebbnd1lem2  22835  chebbnd1lem3  22836  mulog2sumlem2  22900  selberglem2  22911  chpdifbndlem1  22918  chpdifbndlem2  22919  pntrmax  22929  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem1  22954  pntibndlem2  22956  pntibndlem3  22957  pntlemd  22959  pntlemc  22960  pntlema  22961  pntlemg  22963  pntlemr  22967  pntlemj  22968  ostth2lem2  22999  ostth2lem3  23000  ostth2lem4  23001  ostth2  23002  ostth3  23003  tgelrnln  23158  mirauto  23204  eleesub  23292  axsegconlem2  23299  axsegconlem8  23305  axlowdimlem7  23329  axlowdimlem17  23339  usgrares1  23458  usgrafilem2  23460  cusgraexilem1  23509  cusgrares  23515  cusgrasizeinds  23519  cusgrafilem3  23524  wlks  23560  trls  23570  grpoinvfval  23846  grpodivfval  23864  gxfval  23879  ghgrp  23990  isvc  24094  isnv  24125  imsmet  24217  smcnlem  24227  minvecolem2  24411  minvecolem3  24412  minvecolem4c  24415  minvecolem4  24416  minvecolem5  24417  minvecolem6  24418  hhssabloi  24798  pjhthlem1  24929  pjoc1i  24969  cnlnadjlem3  25608  cnlnadjlem5  25610  mdsymlem1  25942  mdsymlem3  25944  abrexexd  26025  elovimad  26090  gsumle  26380  gsummpt2co  26383  ordtconlem1  26488  xrge0pluscn  26504  prsiga  26708  inelsiga  26712  mbfmcst  26808  mbfmco  26813  mbfmcnt  26817  dya2icoseg  26826  sibf0  26854  sibff  26856  sibfinima  26859  sibfof  26860  sitgclg  26862  eulerpartlemt  26888  sseqval  26905  0rrv  26968  rrvsum  26971  signsplypnf  27085  signsply0  27086  signsvtn0  27105  signstfveq0a  27111  signstfveq0  27112  signsvtp  27118  signsvtn  27119  signsvfpn  27120  signsvfnn  27121  erdsze2lem1  27225  erdsze2lem2  27226  txsconlem  27263  cvxpcon  27265  cvxscon  27266  cvmsiota  27300  cvmliftiota  27324  cvmlift2lem10  27335  ghomgrp  27443  wsucex  27897  wsuccl  27898  nobndlem2  27968  nofulllem4  27980  altxpsspw  28142  hfuni  28356  fin2so  28554  mbfresfi  28576  mbfposadd  28577  cnambfre  28578  itg2addnclem2  28582  ibladdnclem  28586  itgaddnclem1  28588  iblabsnclem  28593  iblmulc2nc  28595  itggt0cn  28602  ftc1cnnclem  28603  ftc1anclem3  28607  ftc1anclem5  28609  ftc1anclem8  28612  ftc1anc  28613  locfindis  28715  tailf  28734  tailfb  28736  supex2g  28769  sdclem1  28777  constcncf  28796  sub1cncf  28798  sub2cncf  28799  sstotbnd2  28811  equivbnd2  28829  ismtyres  28845  rrnheibor  28874  reheibor  28876  iccbnd  28877  icccmpALT  28878  exidres  28881  exidresid  28882  mzpnegmpt  29218  vdioph  29256  3anrabdioph  29259  3orrabdioph  29260  rexrabdioph  29270  rexfrabdioph  29271  2rexfrabdioph  29272  3rexfrabdioph  29273  4rexfrabdioph  29274  6rexfrabdioph  29275  7rexfrabdioph  29276  elnnrabdioph  29283  dvdsrabdioph  29286  eldioph4b  29288  pellfundgt1  29362  jm2.27c  29494  lsmfgcl  29565  lmhmfgima  29575  lmhmlnmsplit  29578  pwssplit4  29580  pwslnm  29585  areaquad  29730  sblpnf  29734  fsumcnf  29881  refsum2cnlem1  29897  fmulcl  29900  itgsin0pilem1  29928  itgsinexplem1  29932  stoweidlem2  29935  stoweidlem3  29936  stoweidlem5  29938  stoweidlem16  29949  stoweidlem18  29951  stoweidlem20  29953  stoweidlem21  29954  stoweidlem22  29955  stoweidlem23  29956  stoweidlem31  29964  stoweidlem32  29965  stoweidlem35  29968  stoweidlem36  29969  stoweidlem40  29973  stoweidlem41  29974  stoweidlem47  29980  stoweidlem50  29983  stoweidlem57  29990  stoweidlem59  29992  stoweidlem60  29993  stoweidlem62  29995  wallispi2lem2  30005  el2xptp0  30265  otel3xp  30266  fsumz  30374  fsummsndifre  30375  fsummmodsndifre  30377  fsummsnunz  30379  fsummmodsnunre  30381  qerclwwlknfi  30641  hashclwwlkn0  30642  hashwwlkext  30703  frgrawopreglem1  30775  mptcfsupp  30932  fsuppmapnn0fiublem  30936  fsuppmapnn0fiub  30937  coe1fzgsumdlem  30979  linply1  30999  lincext1  31095  lincext2  31096  lindslinindimp2lem1  31099  lincresunit1  31118  lincresunit2  31119  pmatcollpwscmatlem2  31246  mp2pm2mplem4  31264  chmacl  31282  cpmidgsum  31322  cpmidgsumm2pm  31323  cpmidpmatlem2  31325  cpmidpmatlem3  31326  chcoeffeqlem  31340  cayhamlem3  31342  dp2cl  31400  bnj893  32221  bnj944  32231  bnj969  32239  bnj1136  32288  bnj1177  32297  bnj1452  32343  bnj1489  32347  bj-snglex  32766  bj-projex  32788  bj-pr1ex  32799  bj-1uplex  32801  bj-pr2ex  32813  bj-2uplex  32815  lshpinN  32940  dalemdea  33612  dalem5  33617  dalem8  33620  dalem9  33622  dalem15  33628  dalem23  33646  cdlemblem  33743  osumcllem1N  33906  osumcllem9N  33914  pexmidlem6N  33925  lhpat2  33995  arglem1N  34140  cdleme0aa  34160  cdleme1b  34176  cdleme1  34177  cdleme2  34178  cdleme3b  34179  cdleme3e  34182  cdleme3h  34185  cdleme7b  34194  cdleme7e  34197  cdleme7ga  34198  cdleme9b  34202  cdleme15d  34227  cdleme22gb  34244  cdlemedb  34247  cdlemeda  34248  cdleme23b  34300  cdleme25cl  34307  cdleme27cl  34316  cdleme29cl  34327  cdlemefs27cl  34363  cdleme42c  34422  cdleme42h  34432  cdleme42i  34433  cdlemg4c  34562  cdlemg4  34567  cdlemg6c  34570  cdlemkvcl  34792  cdlemkoatnle  34801  cdlemk14  34804  cdlemk15  34805  cdlemk29-3  34861  cdlemk37  34864  dia2dimlem1  35015  dvheveccl  35063  diblss  35121  dihglblem5  35249  dih1dimatlem  35280  dihat  35286  dihjatcclem1  35369  dihjatcclem2  35370  dihjatcclem4  35372  dochexmidlem5  35415  dochexmidlem6  35416  lclkrlem2m  35470  lclkrlem2o  35472  lcfrlem3  35495  lcfrlem22  35515  lcfrlem25  35518  lcfrlem30  35523  lcfrlem37  35530  mapdpglem17N  35639  mapdpglem19  35641  hdmap1val  35750
  Copyright terms: Public domain W3C validator