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

Theorem syl5eqel 2549
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 2545 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1395    e. wcel 1819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-cleq 2449  df-clel 2452
This theorem is referenced by:  syl5eqelr  2550  3eltr4g  2563  csbexg  4589  csbexgOLD  4591  rabexd  4608  snex  4697  otel3xp  5044  dmresexg  5306  riotaprop  6281  elovimad  6336  fovrn  6444  fnovrn  6449  ovima0  6453  f1oabexg  6758  cofunexg  6763  cofunex2g  6764  abrexex2g  6776  xpexgALT  6792  el2xptp0  6843  opiota  6858  fnwelem  6914  mptsuppdifd  6940  fvmpt2curryd  7018  tfrlem12  7076  rdgseg  7106  oelim2  7262  oeeulem  7268  ecexg  7333  qsexg  7387  pmex  7443  resixpfo  7526  elixpsn  7527  unxpdomlem3  7745  rabfi  7763  fnfi  7816  rnfi  7823  iunfi  7826  unifi  7827  pwfilem  7832  fsuppun  7866  fsuppcolem  7878  mapfienlem2  7883  supexd  7930  cantnfp1lem1  8114  oemapvali  8120  mapfienOLD  8155  wemapwe  8156  wemapweOLD  8157  cnfcomlem  8160  cnfcom  8161  cnfcom2lem  8162  cnfcom2  8163  cnfcom3lem  8164  cnfcom3  8165  cnfcomlemOLD  8168  cnfcomOLD  8169  cnfcom2lemOLD  8170  cnfcom2OLD  8171  cnfcom3lemOLD  8172  cnfcom3OLD  8173  prwf  8246  scott0  8321  htalem  8331  infxpenlem  8408  dfac8b  8429  cfss  8662  cofsmo  8666  coftr  8670  fin1a2lem10  8806  hsmexlem4  8826  hsmex2  8830  fpwwe  9041  canthwelem  9045  pwfseqlem1  9053  wuntp  9106  wunsn  9111  wunsuc  9112  wunr1om  9114  wunot  9118  r1limwun  9131  tsk1  9159  tsk2  9160  tskr1om  9162  gruuni  9195  grusn  9199  gruina  9213  wuncn  9564  negcl  9839  peano5nni  10559  peano5uzi  10972  quoremz  11984  quoremnn0  11985  quoremnn0ALT  11986  intfrac2  11987  intfracq  11988  fsuppmapnn0fiublem  12098  fsuppmapnn0fiub  12099  seqf1olem1  12148  seqf1olem2  12149  serle  12164  discr1  12304  swrdccatin2  12723  swrdccatin12lem2  12725  swrdccatin12  12727  swrdccat3  12728  swrdccat3a  12730  cats1cld  12831  sqrlem4  13090  sqreulem  13203  reccn2  13430  fsumzcl2  13571  fsummsnunz  13580  fsump1i  13595  fsumabs  13626  o1fsum  13638  supcvg  13678  mertenslem1  13704  mertenslem2  13705  rpnnen2  13970  ruclem12  13985  bitsfzolem  14095  bezoutlem2  14188  algrf  14213  algcvg  14216  algcvga  14219  algfx  14220  eucalgcvga  14226  eucalg  14227  prmdiv  14326  pythagtriplem11  14360  pythagtriplem13  14362  pcprecl  14374  infpnlem1  14439  infpnlem2  14440  4sqlem5  14471  mul4sqlem  14482  4sqlem13  14486  4sqlem14  14487  4sqlem17  14490  4sqlem18  14491  vdwlem5  14514  wunndx  14659  wunress  14710  1strwunbndx  14749  restid  14850  mreexdomd  15065  acsfn0  15076  acsfn1  15077  acsfn2  15079  rcaninv  15209  funcf2  15283  funcpropd  15315  fthepi  15343  ressffth  15353  elhomai2  15439  catcxpccl  15602  diag1cl  15637  yonedalem1  15667  prdsinvlem  16304  subggrp  16330  nsgacs  16363  ghmima  16413  gimco  16442  gicref  16445  cntrnsg  16505  oppgmnd  16515  cayley  16565  symgfixfolem1  16589  pmtrdifellem1  16627  psgndmsubg  16653  efgredlemf  16885  efgredlemd  16888  efgredlemc  16889  cycsubgcyg  17029  gsumzaddlem  17060  gsumzaddlemOLD  17062  gsum2dlem1  17123  gsum2dlem2  17124  gsum2dOLD  17126  dprdfid  17183  dprdfidOLD  17190  dprd2dlem1  17216  dprd2da  17217  ablfacrplem  17242  ablfacrp  17243  ablfacrp2  17244  ablfac1lem  17245  pgpfac1lem1  17251  pgpfac1lem2  17252  pgpfac1lem3a  17253  pgpfac1lem3  17254  pgpfac1lem4  17255  pgpfac1lem5  17256  pgpfaclem1  17258  ablfaclem3  17264  opprring  17406  subrgring  17558  lmhmkerlss  17823  rlmlmod  17977  lidl0cl  17985  lidlacl  17986  lidlnegcl  17987  lidlmcl  17991  lidlacs  17995  fidomndrnglem  18081  gsumbagdiag  18154  psrass1lem  18155  psrlidm  18182  psrridm  18184  mplsubrglem  18226  mplsubrglemOLD  18227  vr1cl2  18358  vr1cl  18384  subrgvr1cl  18429  coe1fzgsumdlem  18469  evl1rhm  18494  evl1gsumdlem  18518  zringlpirlem2  18636  zringlpirlem3  18637  zlpirlem2  18641  zlpirlem3  18642  cygznlem1  18731  cygznlem2a  18732  cygznlem3  18734  isphld  18815  lindsmm  18989  mpt2matmul  19074  scmatscmiddistr  19136  scmatf  19157  1marepvmarrepid  19203  1marepvsma1  19211  mdetleib2  19216  smadiadetlem3  19296  cramerimplem1  19311  cramerimplem2  19312  cramerimplem3  19313  cramerimp  19314  pmatcollpwscmatlem2  19417  pmatcollpwscmat  19418  mp2pm2mplem4  19436  chmatcl  19455  cpmidgsum  19495  cpmidgsumm2pm  19496  cpmidpmatlem2  19498  cpmidpmatlem3  19499  chcoeffeqlem  19512  cayhamlem3  19514  topopn  19541  rintopn  19544  fctop  19631  topcld  19662  intcld  19667  uncld  19668  unicld  19673  mretopd  19719  neiptoptop  19758  tgrest  19786  restin  19793  neitr  19807  restcls  19808  restntr  19809  restlp  19810  restperf  19811  perfopn  19812  ordtbaslem  19815  ordtuni  19817  ordtbas2  19818  ordtbas  19819  ordttopon  19820  ordtopn1  19821  ordtopn2  19822  ordtrest2lem  19830  ordtrest2  19831  cnco  19893  cnrest  19912  cnprest2  19917  lmss  19925  cncmp  20018  imacmp  20023  fiuncmp  20030  concompcon  20058  cldllycmp  20121  hausmapdom  20126  lfinun  20151  locfindis  20156  kgentopon  20164  1stckgen  20180  ptbasin  20203  ptbasfi  20207  pttopon  20222  xkotopon  20226  txbasval  20232  ptpjcn  20237  ptcldmpt  20240  dfac14lem  20243  txcn  20252  ptcn  20253  ptrescn  20265  txkgen  20278  cnmpt12f  20292  xkofvcn  20310  qtopval2  20322  elqtop  20323  qtoptop2  20325  hmeoco  20398  idhmeo  20399  ordthmeolem  20427  ptunhmeo  20434  xkohmeo  20441  qtopf1  20442  cfinfil  20519  ufprim  20535  ufildr  20557  fin1aufil  20558  fmfg  20575  elfm3  20576  fbflim  20602  flimclslem  20610  flffbas  20621  cnpflf2  20626  flfcnp2  20633  fclsbas  20647  alexsublem  20669  ptcmplem3  20679  ptcmpg  20682  cnextcn  20692  tgpsubcn  20714  tmdgsum  20719  symgtgp  20725  tmdlactcn  20726  submtmd  20728  clssubg  20732  qustgplem  20744  prdstmdd  20747  tsmsfbas  20751  eltsms  20756  tsmssubm  20769  dvrcn  20811  utop2nei  20878  utop3cls  20879  utopreg  20880  blres  21059  prdsbl  21119  metrest  21152  metustexhalfOLD  21191  metustexhalf  21192  subgngp  21274  nlmvscnlem2  21319  nlmvscnlem1  21320  nrginvrcnlem  21324  qtopbaslem  21390  tgqioo  21430  icccmplem2  21453  icccmp  21455  reconnlem2  21457  xrge0tsms  21464  nmcn  21474  metnrmlem2  21489  divcn  21497  fsumcn  21499  fsum2cn  21500  cncfmet  21537  addccncf  21545  cnmpt2pc  21553  icchmeo  21566  cnrehmeo  21578  cnheiborlem  21579  bndth  21583  lebnumlem2  21587  htpycom  21601  htpyid  21602  htpyco1  21603  htpycc  21605  reparphti  21622  pcohtpylem  21644  pcoptcl  21646  pcoass  21649  pcorevcl  21650  pcorevlem  21651  ipcnlem2  21809  ipcnlem1  21810  cmsss  21914  minveclem4c  21965  minveclem3b  21968  minveclem4a  21970  minveclem4  21972  minveclem6  21974  pjthlem1  21977  ivthlem2  21989  ivthlem3  21990  ovolicc2lem4  22056  finiunmbl  22079  voliunlem1  22085  ioombl1lem1  22093  ioombl1lem3  22095  ioombl1lem4  22096  ovolioo  22103  opnmblALT  22137  mbfimaicc  22165  mbfid  22168  mbfeqalem  22174  mbfres  22176  cncombf  22190  mbfi1flim  22255  itg2monolem2  22283  itg2monolem3  22284  itg2mono  22285  itg2cnlem1  22293  itgcl  22315  iblss  22336  itgeqa  22345  itgss3  22346  itgless  22348  iblconst  22349  ibladdlem  22351  itgaddlem1  22354  iblabslem  22359  iblabsr  22361  iblmulc2  22362  itggt0  22373  itgcn  22374  limcvallem  22400  limcflflem  22409  limcres  22415  cnplimc  22416  limccnp  22420  limccnp2  22421  dvreslem  22438  dvres2lem  22439  dvcnp  22447  dvnff  22451  dvmptres2  22490  dvmptres  22491  dvmptntr  22499  dvmptfsum  22501  dvcnvlem  22502  dvcnv  22503  dvferm1lem  22510  dvferm2lem  22512  dvlipcn  22520  dvlip2  22521  c1liplem1  22522  lhop1lem  22539  dvcnvrelem2  22544  dvcvx  22546  dvfsumge  22548  dvfsumlem3  22554  ftc1lem3  22564  ftc1lem4  22565  mdegleb  22589  ply1remlem  22688  ply0  22730  plyid  22731  plyeq0lem  22732  dgrub  22756  dgrub2  22757  dgrlb  22758  coeidlem  22759  coeaddlem  22771  coemullem  22772  coemulhi  22776  dgreq0  22787  dgrlt  22788  dgradd2  22790  dgrmul  22792  dgrcolem2  22796  dgrco  22797  plycj  22799  coecj  22800  plydivlem2  22815  plydivlem4  22817  plyremlem  22825  plyrem  22826  quotcan  22830  vieta1lem1  22831  elqaalem2  22841  elqaalem3  22842  radcnvcl  22937  psercnlem1  22945  pserdvlem2  22948  pilem2  22972  pilem3  22973  efabl  23062  efsubm  23063  logfac  23110  logcnlem2  23149  logcnlem3  23150  logcnlem4  23151  dvlog  23157  cxpcn  23244  cxpcn3lem  23246  ang180lem1  23266  ang180lem2  23267  ang180lem3  23268  pythag  23274  heron  23294  quart1lem  23311  xrlimcnp  23423  efrlim  23424  ftalem1  23471  ftalem2  23472  ftalem4  23474  ftalem5  23475  basellem1  23479  basellem2  23480  basellem3  23481  basellem4  23482  basellem5  23483  basellem8  23486  dchr1cl  23651  dchrinvcl  23653  dchrptlem1  23664  dchrptlem2  23665  bposlem3  23686  bposlem5  23688  bposlem6  23689  lgsqrlem2  23742  lgsqrlem3  23743  lgsqrlem4  23744  lgseisenlem1  23749  lgseisenlem2  23750  lgseisenlem3  23751  lgseisenlem4  23752  lgsquadlem1  23754  lgsquadlem2  23755  lgsquadlem3  23756  2sqlem8  23772  chebbnd1lem1  23779  chebbnd1lem2  23780  chebbnd1lem3  23781  mulog2sumlem2  23845  selberglem2  23856  chpdifbndlem1  23863  chpdifbndlem2  23864  pntrmax  23874  pntpbnd1a  23895  pntpbnd1  23896  pntpbnd2  23897  pntibndlem1  23899  pntibndlem2  23901  pntibndlem3  23902  pntlemd  23904  pntlemc  23905  pntlema  23906  pntlemg  23908  pntlemr  23912  pntlemj  23913  ostth2lem2  23944  ostth2lem3  23945  ostth2lem4  23946  ostth2  23947  ostth3  23948  tgelrnln  24135  mirauto  24186  lmiisolem  24286  eleesub  24340  axsegconlem2  24347  axsegconlem8  24353  axlowdimlem7  24377  axlowdimlem17  24387  usgrares1  24536  usgrafilem2  24538  cusgrares  24598  cusgrasizeinds  24602  cusgrafilem3  24607  wlks  24645  trls  24664  hashwwlkext  24872  qerclwwlknfi  24955  hashclwwlkn0  24956  frgrawopreglem1  25170  grpoinvfval  25352  grpodivfval  25370  gxfval  25385  ghgrpOLD  25496  isvc  25600  isnv  25631  imsmet  25723  smcnlem  25733  minvecolem2  25917  minvecolem3  25918  minvecolem4c  25921  minvecolem4  25922  minvecolem5  25923  minvecolem6  25924  hhssabloi  26304  pjhthlem1  26435  pjoc1i  26475  cnlnadjlem3  27114  cnlnadjlem5  27116  mdsymlem1  27448  mdsymlem3  27450  abrexexd  27534  acunirnmpt  27647  acunirnmpt2  27648  acunirnmpt2f  27649  aciunf1lem  27650  imafi2  27677  gsumle  27922  gsummpt2co  27923  ordtconlem1  28059  xrge0pluscn  28075  prsiga  28292  inelsiga  28296  mbfmcst  28391  mbfmco  28396  mbfmcnt  28400  dya2icoseg  28409  sibf0  28451  sibff  28453  sibfinima  28456  sibfof  28457  sitgclg  28459  eulerpartlemt  28485  sseqval  28502  0rrv  28565  rrvsum  28568  signsplypnf  28682  signsply0  28683  signsvtn0  28702  signstfveq0a  28708  signstfveq0  28709  signsvtp  28715  signsvtn  28716  signsvfpn  28717  signsvfnn  28718  erdsze2lem1  28822  erdsze2lem2  28823  txsconlem  28860  cvxpcon  28862  cvxscon  28863  cvmsiota  28897  cvmliftiota  28921  cvmlift2lem10  28932  ghomgrp  29205  wsucex  29556  wsuccl  29557  nobndlem2  29627  nofulllem4  29639  altxpsspw  29789  hfuni  30003  fin2so  30202  mbfresfi  30223  mbfposadd  30224  cnambfre  30225  itg2addnclem2  30229  ibladdnclem  30233  itgaddnclem1  30235  iblabsnclem  30240  iblmulc2nc  30242  itggt0cn  30249  ftc1cnnclem  30250  ftc1anclem3  30254  ftc1anclem5  30256  ftc1anclem8  30259  ftc1anc  30260  tailf  30355  tailfb  30357  supex2g  30390  sdclem1  30398  constcncf  30417  sub1cncf  30419  sub2cncf  30420  sstotbnd2  30432  equivbnd2  30450  ismtyres  30466  rrnheibor  30495  reheibor  30497  iccbnd  30498  icccmpALT  30499  exidres  30502  exidresid  30503  mzpnegmpt  30838  vdioph  30875  3anrabdioph  30878  3orrabdioph  30879  rexrabdioph  30889  rexfrabdioph  30890  2rexfrabdioph  30891  3rexfrabdioph  30892  4rexfrabdioph  30893  6rexfrabdioph  30894  7rexfrabdioph  30895  elnnrabdioph  30902  dvdsrabdioph  30905  eldioph4b  30907  pellfundgt1  30981  jm2.27c  31111  lsmfgcl  31182  lmhmfgima  31192  lmhmlnmsplit  31195  pwssplit4  31197  pwslnm  31202  areaquad  31346  sblpnf  31352  fsumcnf  31557  rnmptfi  31608  suprnmpt  31612  fzisoeu  31661  upbdrech  31666  upbdrech2  31669  fmulcl  31736  fprodcllemf  31752  ellimciota  31781  constlimc  31791  sumnnodd  31797  addccncf2  31839  cncfiooicclem1  31857  dvresntr  31874  ioodvbdlimc1lem1  31889  ioodvbdlimc1lem2  31890  ioodvbdlimc2lem  31892  dvnmul  31901  itgsin0pilem1  31909  itgsinexplem1  31913  mbfres2cn  31918  iblsplit  31926  iblsplitf  31930  stoweidlem2  31945  stoweidlem3  31946  stoweidlem5  31948  stoweidlem16  31959  stoweidlem18  31961  stoweidlem20  31963  stoweidlem21  31964  stoweidlem22  31965  stoweidlem23  31966  stoweidlem31  31974  stoweidlem32  31975  stoweidlem36  31979  stoweidlem40  31983  stoweidlem41  31984  stoweidlem47  31990  stoweidlem50  31993  stoweidlem57  32000  stoweidlem59  32002  stoweidlem60  32003  stoweidlem62  32005  wallispi2lem2  32015  dirkertrigeqlem1  32041  dirkeritg  32045  dirkercncflem1  32046  dirkercncflem4  32049  fourierdlem4  32054  fourierdlem6  32056  fourierdlem7  32057  fourierdlem19  32069  fourierdlem20  32070  fourierdlem25  32075  fourierdlem26  32076  fourierdlem30  32080  fourierdlem31  32081  fourierdlem32  32082  fourierdlem33  32083  fourierdlem35  32085  fourierdlem36  32086  fourierdlem41  32091  fourierdlem42  32092  fourierdlem47  32097  fourierdlem48  32098  fourierdlem49  32099  fourierdlem50  32100  fourierdlem51  32101  fourierdlem52  32102  fourierdlem54  32104  fourierdlem62  32112  fourierdlem63  32113  fourierdlem64  32114  fourierdlem65  32115  fourierdlem71  32121  fourierdlem76  32126  fourierdlem79  32129  fourierdlem80  32130  fourierdlem85  32135  fourierdlem86  32136  fourierdlem87  32137  fourierdlem89  32139  fourierdlem90  32140  fourierdlem91  32141  fourierdlem94  32144  fourierdlem97  32147  fourierdlem102  32152  fourierdlem103  32153  fourierdlem104  32154  fourierdlem107  32157  fourierdlem113  32163  fourierdlem114  32164  fourierswlem  32174  fouriersw  32175  elaa2lem  32177  etransclem23  32201  etransclem43  32221  etransclem45  32223  etransclem46  32224  etransclem47  32225  etransclem48  32226  pfxccatin12lem2  32500  pfxccatin12  32501  pfxccat3  32502  pfxccatpfx2  32504  pfxccat3a  32505  fsummsndifre  32565  fsummmodsndifre  32567  fsummmodsnunz  32568  usgrafisbaseALT  32660  usgrafisbaseALT2  32661  usgfislem2  32665  usgfisALTlem2  32669  rnghmsscmap2  32883  rhmsscmap2  32929  rhmsscrnghm  32936  fldc  32993  fldhmsubc  32994  fldcOLD  33012  fldhmsubcOLD  33013  mptcfsupp  33075  linply1  33095  lincext1  33157  lincext2  33158  lindslinindimp2lem1  33161  lincresunit1  33180  lincresunit2  33181  dp2cl  33265  aacllem  33318  bnj893  34087  bnj944  34097  bnj969  34105  bnj1136  34154  bnj1177  34163  bnj1452  34209  bnj1489  34213  bj-snglex  34632  bj-projex  34654  bj-pr1ex  34665  bj-1uplex  34667  bj-pr2ex  34679  bj-2uplex  34681  lshpinN  34815  dalemdea  35487  dalem5  35492  dalem8  35495  dalem9  35497  dalem15  35503  dalem23  35521  cdlemblem  35618  osumcllem1N  35781  osumcllem9N  35789  pexmidlem6N  35800  lhpat2  35870  arglem1N  36016  cdleme0aa  36036  cdleme1b  36052  cdleme1  36053  cdleme2  36054  cdleme3b  36055  cdleme3e  36058  cdleme3h  36061  cdleme7b  36070  cdleme7e  36073  cdleme7ga  36074  cdleme9b  36078  cdleme15d  36103  cdleme22gb  36120  cdlemedb  36123  cdlemeda  36124  cdleme23b  36177  cdleme25cl  36184  cdleme27cl  36193  cdleme29cl  36204  cdlemefs27cl  36240  cdleme42c  36299  cdleme42h  36309  cdleme42i  36310  cdlemg4c  36439  cdlemg4  36444  cdlemg6c  36447  cdlemkvcl  36669  cdlemkoatnle  36678  cdlemk14  36681  cdlemk15  36682  cdlemk29-3  36738  cdlemk37  36741  dia2dimlem1  36892  dvheveccl  36940  diblss  36998  dihglblem5  37126  dih1dimatlem  37157  dihat  37163  dihjatcclem1  37246  dihjatcclem2  37247  dihjatcclem4  37249  dochexmidlem5  37292  dochexmidlem6  37293  lclkrlem2m  37347  lclkrlem2o  37349  lcfrlem3  37372  lcfrlem22  37392  lcfrlem25  37395  lcfrlem30  37400  lcfrlem37  37407  mapdpglem17N  37516  mapdpglem19  37518  hdmap1val  37627
  Copyright terms: Public domain W3C validator