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

Theorem syl5eqel 2559
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 2555 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  syl5eqelr  2560  3eltr4g  2573  csbexg  4579  csbexgOLD  4581  rabexd  4599  snex  4688  otel3xp  5034  dmresexg  5294  riotaprop  6267  elovimad  6320  fovrn  6427  fnovrn  6432  ovima0  6436  f1oabexg  6740  cofunexg  6745  cofunex2g  6746  abrexex2g  6758  xpexgALT  6774  el2xptp0  6825  opiota  6840  fnwelem  6895  mptsuppdifd  6919  fvmpt2curryd  6997  tfrlem12  7055  rdgseg  7085  oelim2  7241  oeeulem  7247  ecexg  7312  qsexg  7366  pmex  7422  resixpfo  7504  elixpsn  7505  unxpdomlem3  7723  rabfi  7741  fnfi  7794  rnfi  7801  iunfi  7804  unifi  7805  pwfilem  7810  fsuppun  7844  fsuppcolem  7856  mapfienlem2  7861  supexd  7909  cantnfp1lem1  8093  oemapvali  8099  mapfienOLD  8134  wemapwe  8135  wemapweOLD  8136  cnfcomlem  8139  cnfcom  8140  cnfcom2lem  8141  cnfcom2  8142  cnfcom3lem  8143  cnfcom3  8144  cnfcomlemOLD  8147  cnfcomOLD  8148  cnfcom2lemOLD  8149  cnfcom2OLD  8150  cnfcom3lemOLD  8151  cnfcom3OLD  8152  prwf  8225  scott0  8300  htalem  8310  infxpenlem  8387  dfac8b  8408  cfss  8641  cofsmo  8645  coftr  8649  fin1a2lem10  8785  hsmexlem4  8805  hsmex2  8809  fpwwe  9020  canthwelem  9024  pwfseqlem1  9032  wuntp  9085  wunsn  9090  wunsuc  9091  wunr1om  9093  wunot  9097  r1limwun  9110  tsk1  9138  tsk2  9139  tskr1om  9141  gruuni  9174  grusn  9178  gruina  9192  wuncn  9543  negcl  9816  peano5nni  10535  peano5uzi  10945  quoremz  11945  quoremnn0  11946  quoremnn0ALT  11947  intfrac2  11948  intfracq  11949  fsuppmapnn0fiublem  12059  fsuppmapnn0fiub  12060  seqf1olem1  12109  seqf1olem2  12110  serle  12125  discr1  12264  swrdccatin2  12669  swrdccatin12lem2  12671  swrdccatin12  12673  swrdccat3  12674  swrdccat3a  12676  cats1cld  12777  sqrlem4  13036  sqreulem  13148  reccn2  13375  fsumzcl2  13516  fsummsnunz  13525  fsump1i  13540  fsumabs  13571  o1fsum  13583  supcvg  13623  mertenslem1  13649  mertenslem2  13650  rpnnen2  13813  ruclem12  13828  bitsfzolem  13936  bezoutlem2  14029  algrf  14054  algcvg  14057  algcvga  14060  algfx  14061  eucalgcvga  14067  eucalg  14068  prmdiv  14167  pythagtriplem11  14201  pythagtriplem13  14203  pcprecl  14215  infpnlem1  14280  infpnlem2  14281  4sqlem5  14312  mul4sqlem  14323  4sqlem13  14327  4sqlem14  14328  4sqlem17  14331  4sqlem18  14332  vdwlem5  14355  wunndx  14499  wunress  14547  restid  14682  mreexdomd  14897  acsfn0  14908  acsfn1  14909  acsfn2  14911  funcf2  15088  funcpropd  15120  fthepi  15148  ressffth  15158  elhomai2  15212  catcxpccl  15327  diag1cl  15362  yonedalem1  15392  prdsinvlem  15975  subggrp  15996  nsgacs  16029  ghmima  16079  gimco  16108  gicref  16111  cntrnsg  16171  oppgmnd  16181  cayley  16231  symgfixfolem1  16256  pmtrdifellem1  16294  psgndmsubg  16320  efgredlemf  16552  efgredlemd  16555  efgredlemc  16556  cycsubgcyg  16691  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsum2dlem1  16785  gsum2dlem2  16786  gsum2dOLD  16788  dprdfid  16844  dprdfidOLD  16851  dprd2dlem1  16877  dprd2da  16878  ablfacrplem  16903  ablfacrp  16904  ablfacrp2  16905  ablfac1lem  16906  pgpfac1lem1  16912  pgpfac1lem2  16913  pgpfac1lem3a  16914  pgpfac1lem3  16915  pgpfac1lem4  16916  pgpfac1lem5  16917  pgpfaclem1  16919  ablfaclem3  16925  opprrng  17061  subrgrng  17212  lmhmkerlss  17477  rlmlmod  17631  lidl0cl  17639  lidlacl  17640  lidlnegcl  17641  lidlmcl  17644  lidlacs  17648  fidomndrnglem  17723  gsumbagdiag  17796  psrass1lem  17797  psrlidm  17824  psrridm  17826  mplsubrglem  17868  mplsubrglemOLD  17869  vr1cl2  18000  vr1cl  18026  subrgvr1cl  18071  coe1fzgsumdlem  18111  evl1rhm  18136  evl1gsumdlem  18160  zringlpirlem2  18274  zringlpirlem3  18275  zlpirlem2  18279  zlpirlem3  18280  cygznlem1  18369  cygznlem2a  18370  cygznlem3  18372  isphld  18453  lindsmm  18627  scmatscmiddistr  18774  scmatf  18795  1marepvmarrepid  18841  1marepvsma1  18849  mdetleib2  18854  smadiadetlem3  18934  cramerimplem1  18949  cramerimplem2  18950  cramerimplem3  18951  cramerimp  18952  pmatcollpwscmatlem2  19055  pmatcollpwscmat  19056  mp2pm2mplem4  19074  chmatcl  19093  cpmidgsum  19133  cpmidgsumm2pm  19134  cpmidpmatlem2  19136  cpmidpmatlem3  19137  chcoeffeqlem  19150  cayhamlem3  19152  topopn  19179  rintopn  19182  fctop  19268  topcld  19299  intcld  19304  uncld  19305  unicld  19310  mretopd  19356  neiptoptop  19395  tgrest  19423  restin  19430  neitr  19444  restcls  19445  restntr  19446  restlp  19447  restperf  19448  perfopn  19449  ordtbaslem  19452  ordtuni  19454  ordtbas2  19455  ordtbas  19456  ordttopon  19457  ordtopn1  19458  ordtopn2  19459  ordtrest2lem  19467  ordtrest2  19468  cnco  19530  cnrest  19549  cnprest2  19554  lmss  19562  cncmp  19655  imacmp  19660  fiuncmp  19667  bwthOLD  19674  concompcon  19696  cldllycmp  19759  hausmapdom  19764  kgentopon  19771  1stckgen  19787  ptbasin  19810  ptbasfi  19814  pttopon  19829  xkotopon  19833  txbasval  19839  ptpjcn  19844  ptcldmpt  19847  dfac14lem  19850  txcn  19859  ptcn  19860  ptrescn  19872  txkgen  19885  cnmpt12f  19899  xkofvcn  19917  qtopval2  19929  elqtop  19930  qtoptop2  19932  hmeoco  20005  idhmeo  20006  ordthmeolem  20034  ptunhmeo  20041  xkohmeo  20048  qtopf1  20049  cfinfil  20126  ufprim  20142  ufildr  20164  fin1aufil  20165  fmfg  20182  elfm3  20183  fbflim  20209  flimclslem  20217  flffbas  20228  cnpflf2  20233  flfcnp2  20240  fclsbas  20254  alexsublem  20276  ptcmplem3  20286  ptcmpg  20289  cnextcn  20299  tgpsubcn  20321  tmdgsum  20326  symgtgp  20332  tmdlactcn  20333  submtmd  20335  clssubg  20339  divstgplem  20351  prdstmdd  20354  tsmsfbas  20358  eltsms  20363  tsmssubm  20376  dvrcn  20418  utop2nei  20485  utop3cls  20486  utopreg  20487  blres  20666  prdsbl  20726  metrest  20759  metustexhalfOLD  20798  metustexhalf  20799  subgngp  20881  nlmvscnlem2  20926  nlmvscnlem1  20927  nrginvrcnlem  20931  qtopbaslem  20997  tgqioo  21037  icccmplem2  21060  icccmp  21062  reconnlem2  21064  xrge0tsms  21071  nmcn  21081  metnrmlem2  21096  divcn  21104  fsumcn  21106  fsum2cn  21107  cncfmet  21144  addccncf  21152  cnmpt2pc  21160  icchmeo  21173  cnrehmeo  21185  cnheiborlem  21186  bndth  21190  lebnumlem2  21194  htpycom  21208  htpyid  21209  htpyco1  21210  htpycc  21212  reparphti  21229  pcohtpylem  21251  pcoptcl  21253  pcoass  21256  pcorevcl  21257  pcorevlem  21258  ipcnlem2  21416  ipcnlem1  21417  cmsss  21521  minveclem4c  21572  minveclem3b  21575  minveclem4a  21577  minveclem4  21579  minveclem6  21581  pjthlem1  21584  ivthlem2  21596  ivthlem3  21597  ovolicc2lem4  21663  finiunmbl  21686  voliunlem1  21692  ioombl1lem1  21700  ioombl1lem3  21702  ioombl1lem4  21703  ovolioo  21710  opnmblALT  21744  mbfimaicc  21772  mbfid  21775  mbfeqalem  21781  mbfres  21783  cncombf  21797  mbfi1flim  21862  itg2monolem2  21890  itg2monolem3  21891  itg2mono  21892  itg2cnlem1  21900  itgcl  21922  iblss  21943  itgeqa  21952  itgss3  21953  itgless  21955  iblconst  21956  ibladdlem  21958  itgaddlem1  21961  iblabslem  21966  iblabsr  21968  iblmulc2  21969  itggt0  21980  itgcn  21981  limcvallem  22007  limcflflem  22016  limcres  22022  cnplimc  22023  limccnp  22027  limccnp2  22028  dvreslem  22045  dvres2lem  22046  dvcnp  22054  dvnff  22058  dvmptres2  22097  dvmptres  22098  dvmptntr  22106  dvmptfsum  22108  dvcnvlem  22109  dvcnv  22110  dvferm1lem  22117  dvferm2lem  22119  dvlipcn  22127  dvlip2  22128  c1liplem1  22129  lhop1lem  22146  dvcnvrelem2  22151  dvcvx  22153  dvfsumge  22155  dvfsumlem3  22161  ftc1lem3  22171  ftc1lem4  22172  mdegleb  22196  ply1remlem  22295  ply0  22337  plyid  22338  plyeq0lem  22339  dgrub  22363  dgrub2  22364  dgrlb  22365  coeidlem  22366  coeaddlem  22377  coemullem  22378  coemulhi  22382  dgreq0  22393  dgrlt  22394  dgradd2  22396  dgrmul  22398  dgrcolem2  22402  dgrco  22403  plycj  22405  coecj  22406  plydivlem2  22421  plydivlem4  22423  plyremlem  22431  plyrem  22432  quotcan  22436  vieta1lem1  22437  elqaalem2  22447  elqaalem3  22448  radcnvcl  22543  psercnlem1  22551  pserdvlem2  22554  pilem2  22578  pilem3  22579  logfac  22710  logcnlem2  22749  logcnlem3  22750  logcnlem4  22751  dvlog  22757  cxpcn  22844  cxpcn3lem  22846  ang180lem1  22866  ang180lem2  22867  ang180lem3  22868  pythag  22874  heron  22894  quart1lem  22911  xrlimcnp  23023  efrlim  23024  ftalem1  23071  ftalem2  23072  ftalem4  23074  ftalem5  23075  basellem1  23079  basellem2  23080  basellem3  23081  basellem4  23082  basellem5  23083  basellem8  23086  dchr1cl  23251  dchrinvcl  23253  dchrptlem1  23264  dchrptlem2  23265  bposlem3  23286  bposlem5  23288  bposlem6  23289  lgsqrlem2  23342  lgsqrlem3  23343  lgsqrlem4  23344  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgseisenlem4  23352  lgsquadlem1  23354  lgsquadlem2  23355  lgsquadlem3  23356  2sqlem8  23372  chebbnd1lem1  23379  chebbnd1lem2  23380  chebbnd1lem3  23381  mulog2sumlem2  23445  selberglem2  23456  chpdifbndlem1  23463  chpdifbndlem2  23464  pntrmax  23474  pntpbnd1a  23495  pntpbnd1  23496  pntpbnd2  23497  pntibndlem1  23499  pntibndlem2  23501  pntibndlem3  23502  pntlemd  23504  pntlemc  23505  pntlema  23506  pntlemg  23508  pntlemr  23512  pntlemj  23513  ostth2lem2  23544  ostth2lem3  23545  ostth2lem4  23546  ostth2  23547  ostth3  23548  tgelrnln  23721  mirauto  23766  lmiisolem  23835  eleesub  23887  axsegconlem2  23894  axsegconlem8  23900  axlowdimlem7  23924  axlowdimlem17  23934  usgrares1  24083  usgrafilem2  24085  cusgraexilem1  24139  cusgrares  24145  cusgrasizeinds  24149  cusgrafilem3  24154  wlks  24192  trls  24211  hashwwlkext  24419  qerclwwlknfi  24502  hashclwwlkn0  24503  frgrawopreglem1  24718  grpoinvfval  24899  grpodivfval  24917  gxfval  24932  ghgrp  25043  isvc  25147  isnv  25178  imsmet  25270  smcnlem  25280  minvecolem2  25464  minvecolem3  25465  minvecolem4c  25468  minvecolem4  25469  minvecolem5  25470  minvecolem6  25471  hhssabloi  25851  pjhthlem1  25982  pjoc1i  26022  cnlnadjlem3  26661  cnlnadjlem5  26663  mdsymlem1  26995  mdsymlem3  26997  abrexexd  27078  gsumle  27430  gsummpt2co  27431  ordtconlem1  27539  xrge0pluscn  27555  prsiga  27768  inelsiga  27772  mbfmcst  27867  mbfmco  27872  mbfmcnt  27876  dya2icoseg  27885  sibf0  27913  sibff  27915  sibfinima  27918  sibfof  27919  sitgclg  27921  eulerpartlemt  27947  sseqval  27964  0rrv  28027  rrvsum  28030  signsplypnf  28144  signsply0  28145  signsvtn0  28164  signstfveq0a  28170  signstfveq0  28171  signsvtp  28177  signsvtn  28178  signsvfpn  28179  signsvfnn  28180  erdsze2lem1  28284  erdsze2lem2  28285  txsconlem  28322  cvxpcon  28324  cvxscon  28325  cvmsiota  28359  cvmliftiota  28383  cvmlift2lem10  28394  ghomgrp  28502  wsucex  28956  wsuccl  28957  nobndlem2  29027  nofulllem4  29039  altxpsspw  29201  hfuni  29415  fin2so  29614  mbfresfi  29636  mbfposadd  29637  cnambfre  29638  itg2addnclem2  29642  ibladdnclem  29646  itgaddnclem1  29648  iblabsnclem  29653  iblmulc2nc  29655  itggt0cn  29662  ftc1cnnclem  29663  ftc1anclem3  29667  ftc1anclem5  29669  ftc1anclem8  29672  ftc1anc  29673  locfindis  29775  tailf  29794  tailfb  29796  supex2g  29829  sdclem1  29837  constcncf  29856  sub1cncf  29858  sub2cncf  29859  sstotbnd2  29871  equivbnd2  29889  ismtyres  29905  rrnheibor  29934  reheibor  29936  iccbnd  29937  icccmpALT  29938  exidres  29941  exidresid  29942  mzpnegmpt  30278  vdioph  30315  3anrabdioph  30318  3orrabdioph  30319  rexrabdioph  30329  rexfrabdioph  30330  2rexfrabdioph  30331  3rexfrabdioph  30332  4rexfrabdioph  30333  6rexfrabdioph  30334  7rexfrabdioph  30335  elnnrabdioph  30342  dvdsrabdioph  30345  eldioph4b  30347  pellfundgt1  30421  jm2.27c  30553  lsmfgcl  30624  lmhmfgima  30634  lmhmlnmsplit  30637  pwssplit4  30639  pwslnm  30644  areaquad  30789  sblpnf  30793  fsumcnf  30974  refsum2cnlem1  30990  rnmptfi  31025  suprnmpt  31029  fzisoeu  31077  upbdrech  31082  upbdrech2  31085  fmulcl  31131  ellimciota  31156  sumnnodd  31172  addccncf2  31214  cncfiooicclem1  31232  dvresntr  31246  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgsin0pilem1  31267  itgsinexplem1  31271  stoweidlem2  31302  stoweidlem3  31303  stoweidlem5  31305  stoweidlem16  31316  stoweidlem18  31318  stoweidlem20  31320  stoweidlem21  31321  stoweidlem22  31322  stoweidlem23  31323  stoweidlem31  31331  stoweidlem32  31332  stoweidlem35  31335  stoweidlem36  31336  stoweidlem40  31340  stoweidlem41  31341  stoweidlem47  31347  stoweidlem50  31350  stoweidlem57  31357  stoweidlem59  31359  stoweidlem60  31360  stoweidlem62  31362  wallispi2lem2  31372  dirkertrigeqlem1  31398  dirkeritg  31402  dirkercncflem1  31403  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem4  31411  fourierdlem6  31413  fourierdlem7  31414  fourierdlem19  31426  fourierdlem20  31427  fourierdlem25  31432  fourierdlem26  31433  fourierdlem30  31437  fourierdlem31  31438  fourierdlem32  31439  fourierdlem33  31440  fourierdlem35  31442  fourierdlem36  31443  fourierdlem41  31448  fourierdlem42  31449  fourierdlem45  31452  fourierdlem47  31454  fourierdlem48  31455  fourierdlem49  31456  fourierdlem50  31457  fourierdlem51  31458  fourierdlem52  31459  fourierdlem54  31461  fourierdlem64  31471  fourierdlem65  31472  fourierdlem71  31478  fourierdlem76  31483  fourierdlem79  31486  fourierdlem85  31492  fourierdlem86  31493  fourierdlem87  31494  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem94  31501  fourierdlem102  31509  fourierdlem103  31510  fourierdlem104  31511  fourierdlem107  31514  fourierdlem113  31520  fourierdlem114  31521  fouriersw  31532  fsummsndifre  31814  fsummmodsndifre  31816  fsummmodsnunz  31817  usgrafisbaseALT  31909  usgrafisbaseALT2  31910  usgfislem2  31914  usgfisALTlem2  31918  mptcfsupp  32046  linply1  32066  lincext1  32128  lincext2  32129  lindslinindimp2lem1  32132  lincresunit1  32151  lincresunit2  32152  dp2cl  32244  bnj893  33065  bnj944  33075  bnj969  33083  bnj1136  33132  bnj1177  33141  bnj1452  33187  bnj1489  33191  bj-snglex  33612  bj-projex  33634  bj-pr1ex  33645  bj-1uplex  33647  bj-pr2ex  33659  bj-2uplex  33661  lshpinN  33786  dalemdea  34458  dalem5  34463  dalem8  34466  dalem9  34468  dalem15  34474  dalem23  34492  cdlemblem  34589  osumcllem1N  34752  osumcllem9N  34760  pexmidlem6N  34771  lhpat2  34841  arglem1N  34986  cdleme0aa  35006  cdleme1b  35022  cdleme1  35023  cdleme2  35024  cdleme3b  35025  cdleme3e  35028  cdleme3h  35031  cdleme7b  35040  cdleme7e  35043  cdleme7ga  35044  cdleme9b  35048  cdleme15d  35073  cdleme22gb  35090  cdlemedb  35093  cdlemeda  35094  cdleme23b  35146  cdleme25cl  35153  cdleme27cl  35162  cdleme29cl  35173  cdlemefs27cl  35209  cdleme42c  35268  cdleme42h  35278  cdleme42i  35279  cdlemg4c  35408  cdlemg4  35413  cdlemg6c  35416  cdlemkvcl  35638  cdlemkoatnle  35647  cdlemk14  35650  cdlemk15  35651  cdlemk29-3  35707  cdlemk37  35710  dia2dimlem1  35861  dvheveccl  35909  diblss  35967  dihglblem5  36095  dih1dimatlem  36126  dihat  36132  dihjatcclem1  36215  dihjatcclem2  36216  dihjatcclem4  36218  dochexmidlem5  36261  dochexmidlem6  36262  lclkrlem2m  36316  lclkrlem2o  36318  lcfrlem3  36341  lcfrlem22  36361  lcfrlem25  36364  lcfrlem30  36369  lcfrlem37  36376  mapdpglem17N  36485  mapdpglem19  36487  hdmap1val  36596
  Copyright terms: Public domain W3C validator