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

Theorem syl5ibrcom 222
Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)
Hypotheses
Ref Expression
syl5ibr.1
syl5ibr.2
Assertion
Ref Expression
syl5ibrcom

Proof of Theorem syl5ibrcom
StepHypRef Expression
1 syl5ibr.1 . . 3
2 syl5ibr.2 . . 3
31, 2syl5ibr 221 . 2
43com12 31 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  biimprcd  225  elsnc2g  4059  reusv2lem2  4654  reusv3  4660  alxfr  4665  reuhypd  4679  opth1  4725  euotd  4753  tz7.2  4868  ordtri1  4916  xpsspw  5121  fvmptdv2  5969  fveqressseq  6027  foco2  6051  fsn  6069  fnsnb  6090  fmptsng  6092  fmptsnd  6093  fconst2g  6125  fnprb  6129  fnprOLD  6130  funfvima  6147  soisoi  6224  isores3  6231  eusvobj2  6289  ovmpt2dv2  6436  f1opw2  6528  suppssfvOLD  6531  suppssov1OLD  6532  sorpssun  6587  sorpssin  6588  oneqmin  6640  nlimsucg  6677  onzsl  6681  tfinds  6694  funcnvuni  6753  opiota  6859  mpt2sn  6891  suppssov1  6951  suppssfv  6955  brtpos  6983  seqomlem1  7134  seqomlem2  7135  omordi  7234  omord  7236  omwordi  7239  oeeui  7270  nnmordi  7299  nnmord  7300  nnmwordi  7303  nnawordex  7305  nnaordex  7306  nneob  7320  omsmolem  7321  qsss  7391  eroveu  7425  mapsncnv  7485  ralxpmap  7488  elixpsn  7528  ixpsnf1o  7529  boxcutc  7532  pw2f1olem  7641  2pwne  7693  mapxpen  7703  mapunen  7706  php  7721  unxpdomlem2  7745  en1eqsnbi  7770  isfiniteg  7800  fofinf1o  7821  f1opwfi  7844  elfiun  7910  oieu  7985  brwdom2  8020  wdomtr  8022  ixpiunwdom  8038  en3lplem1  8052  suc11reg  8057  inf3lemd  8065  cantnfvalf  8105  cantnflt  8112  cantnfp1lem3  8120  cantnflem2  8130  cantnfltOLD  8142  cantnfp1lem3OLD  8146  r1tr  8215  dfac8alem  8431  wdomnumr  8466  isinfcard  8494  aceq3lem  8522  dfac5lem4  8528  dfac5  8530  dfac2  8532  coftr  8674  fin23lem28  8741  fin23lem29  8742  fin1a2lem11  8811  fin1a2lem12  8812  fin1a2lem13  8813  hsmexlem9  8826  axdclem  8920  pwcfsdom  8979  gchdomtri  9028  fpwwe2  9042  gchpwdom  9069  gchhar  9078  addnidpi  9300  nqereu  9328  genpv  9398  genpdm  9401  distrlem5pr  9426  mulid1  9614  ltne  9702  mul02  9779  cnegex  9782  mul0or  10214  sup2  10524  supmul1  10533  supmul  10536  creur  10555  creui  10556  cju  10557  nnsub  10599  un0addcl  10854  un0mulcl  10855  nn0sub  10871  elz2  10906  zaddcl  10929  suprzcl2  11201  qmulz  11214  qre  11216  qnegcl  11228  xrmax1  11405  xrmin2  11408  max1ALT  11416  xlesubadd  11484  xmulass  11508  xlemul1a  11509  xrsupexmnf  11525  xrinfmexpnf  11526  xrub  11532  iccid  11603  fzsn  11754  fzsuc2  11766  fz1sbc  11783  elfzp12  11786  seqid3  12151  bcval5  12396  bcpasc  12399  hashbnd  12411  hashnnn0genn0  12416  hashprg  12460  hashfzo  12487  wrdl1s1  12622  cats1un  12701  shftlem  12901  replim  12949  absmod0  13136  absz  13144  rlimdm  13374  summolem2  13538  summo  13539  zsum  13540  fsum  13542  fsummulc2  13599  fsumconst  13605  fsum00  13612  incexclem  13648  isumsplit  13652  infcvgaux1i  13668  prodmolem2  13742  prodmo  13743  zprod  13744  fprod  13748  prodsn  13767  fprodconst  13782  ruclem2  13965  fzo0dvdseq  14039  bitsf1ocnv  14094  sadcaddlem  14107  smueqlem  14140  gcdabs1  14172  bezoutlem1  14176  bezoutlem3  14178  bezoutlem4  14179  dvdsgcd  14181  dvdsmulgcd  14192  dvdsprime  14230  coprm  14241  isprm5  14253  prmdvdsexpr  14257  rpexp  14261  phibndlem  14300  dfphi2  14304  odzdvds  14322  pythagtriplem1  14340  iserodd  14359  pceulem  14369  pcqmul  14377  pcqcl  14380  pcxcl  14384  pcneg  14397  pcabs  14398  pcgcd1  14400  pcz  14404  pcprmpw2  14405  pcprmpw  14406  pcaddlem  14407  pcadd  14408  pcmpt  14411  pockthg  14424  prmreclem5  14438  4sqlem4  14470  mul4sq  14472  vdwapun  14492  vdwlem2  14500  vdwlem6  14504  vdwlem8  14506  vdwlem13  14511  0ram  14538  ram0  14540  ramcl  14547  cshwsiun  14584  wunress  14696  firest  14830  xpscfv  14959  isssc  15189  pospo  15603  latnlej  15698  gsumval2a  15906  mnd1id  15963  mulgnn0p1  16153  mulgnn0ass  16171  gicsubgen  16326  symg1bas  16421  psgnunilem1  16518  psgnunilem2  16520  mndodcongi  16567  oddvdsnn0  16568  odnncl  16569  oddvds  16571  odeq  16574  odeq1  16582  pgpfi2  16626  sylow2a  16639  sylow2blem3  16642  sylow3lem6  16652  lsmelvalm  16671  lsmsubm  16673  lsmsubg  16674  lsmmod  16693  lsmdisj2  16700  efgmnvl  16732  efgtlen  16744  efgs1b  16754  efgrelexlemb  16768  efgredeu  16770  efgcpbllemb  16773  frgpuptinv  16789  frgpup3lem  16795  qusabl  16871  frgpnabllem1  16877  cyggeninv  16886  cyggenod  16887  cygabl  16893  gsumval3eu  16907  dprdssv  17056  dprdfeq0  17062  dprdfeq0OLD  17069  dprdsubg  17071  dprddisj2  17087  dprddisj2OLD  17088  ablfacrp  17117  pgpfac1lem3  17128  pgpfaclem2  17133  dvreq1  17342  irredn1  17355  drngmul0or  17417  isabvd  17469  abvdom  17487  issrngd  17510  lss1d  17609  lspsneq0  17658  lbspss  17728  lsmcl  17729  lvecvs0or  17754  lspindpi  17778  lidl1el  17866  lpiss  17898  lidldvgen  17903  nzrunit  17915  rrgeq0  17938  domneq0  17946  mplsubrglem  18100  mplsubrglemOLD  18101  mplmonmul  18126  mplcoe5lem  18130  coe1tmmul2  18317  coe1tmmul  18318  pf1ind  18391  qsssubdrg  18477  zringlpirlem1  18509  zlpirlem1  18514  znfld  18599  znunit  18602  znrrg  18604  cygznlem3  18608  frgpcyg  18612  psgnghm  18616  ipeq0  18673  cssincl  18719  lsmcss  18723  obselocv  18759  dsmmacl  18772  dsmmlss  18775  mat1dimelbas  18973  mdetralt  19110  mdetunilem2  19115  mdetunilem7  19120  mdetunilem9  19122  maducoeval2  19142  chpscmat  19343  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  istopon  19426  eltg3  19463  tgidm  19482  clsval2  19551  opncldf1  19585  restbas  19659  tgrest  19660  restcld  19673  restcldr  19675  restcls  19682  restntr  19683  ordtbas2  19692  ordtbas  19693  ordtrest2lem  19704  ordtrest2  19705  pnfnei  19721  mnfnei  19722  tgcn  19753  cnconst  19785  cnindis  19793  lmss  19799  ordtt1  19880  discmp  19898  1stcrest  19954  2ndcdisj  19957  cldllycmp  19996  txbas  20068  ptpjpre1  20072  ptuni2  20077  ptbasin  20078  ptbasfi  20082  ptopn2  20085  txbasval  20107  ptpjopn  20113  ptclsg  20116  dfac14lem  20118  xkoccn  20120  ptcnp  20123  upxp  20124  ptrescn  20140  txkgen  20153  xkoptsub  20155  xkopt  20156  xkoco1cn  20158  xkoco2cn  20159  xkococn  20161  xkoinjcn  20188  ordthmeolem  20302  ptuncnv  20308  nrmhaus  20327  fbssint  20339  fbfinnfr  20342  fbasrn  20385  isufil2  20409  filufint  20421  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem3  20457  fmfnfmlem4  20458  fmfnfm  20459  flimtopon  20471  flimclslem  20485  fclstopon  20513  fclscf  20526  flimfnfcls  20529  alexsublem  20544  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem2  20553  tmdgsum2  20595  symgtgp  20600  cldsubg  20609  qustgplem  20619  tgptsmscld  20653  tsmsxplem1  20655  imasdsf1olem  20876  blssps  20927  blss  20928  stdbdxmet  21018  methaus  21023  metrest  21027  nrginvrcn  21200  nmoeq0  21243  blssioo  21300  xrtgioo  21311  xrsxmet  21314  reconnlem1  21331  reconnlem2  21332  xrge0tsms  21339  elcncf1di  21399  iccpnfcnv  21444  evth  21459  lebnumlem1  21461  lebnumlem2  21462  lebnumlem3  21463  nmoleub3  21602  minveclem3b  21843  ivthlem2  21864  ivthlem3  21865  elovolm  21886  ovolmge0  21888  ovoliun  21916  ovolicc2lem3  21930  ovolicc2  21933  voliunlem3  21962  dyaddisj  22005  dyadmax  22007  opnmblALT  22012  ismbfd  22047  ismbf2d  22048  mbfimaopnlem  22062  mbfimaopn2  22064  i1fmullem  22101  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  itg2lcl  22134  itgsplitioo  22244  ellimc2  22281  rolle  22391  dvlip  22394  dvge0  22407  dvne0  22412  lhop1lem  22414  tdeglem4  22458  degltlem1  22472  deg1nn0clb  22490  deg1lt0  22491  dvdsq1p  22561  ply1rem  22564  fta1g  22568  elply2  22593  plyf  22595  ne0p  22604  plyeq0lem  22607  plypf1  22609  0dgrb  22643  coe1termlem  22655  dgrcolem2  22671  plymul0or  22677  plyrem  22701  fta1  22704  quotcan  22705  aalioulem3  22730  eff1olem  22935  lognegb  22974  eflogeq  22986  argregt0  22995  argrege0  22996  tanarg  23004  cxpexp  23049  cxpeq0  23059  mulcxp  23066  cxpeq  23131  atans2  23262  scvxcvx  23315  isppw2  23389  vmappw  23390  vmacl  23392  efvmacl  23394  isnsqf  23409  mumullem2  23454  sqff1o  23456  dvdsppwf1o  23462  ppiublem1  23477  vmalelog  23480  chtublem  23486  fsumvma  23488  perfectlem2  23505  perfect  23506  bposlem1  23559  lgsmod  23596  lgsne0  23608  lgsdirnn0  23614  lgsqr  23621  lgsdchr  23623  lgseisenlem2  23625  lgsquadlem1  23629  lgsquadlem2  23630  2sqlem2  23639  mul2sq  23640  2sqlem7  23645  dchrisum0fno1  23696  pntrsumbnd2  23752  ostthlem1  23812  ostth2lem2  23819  ostth3  23823  ostth  23824  colinearalg  24213  axpasch  24244  axlowdimlem16  24260  axlowdimlem17  24261  axlowdim  24264  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  usgraexmpl  24401  nbgraf1olem1  24441  nbgraf1olem3  24443  nbgraf1olem5  24445  nb3graprlem2  24452  cusgrasize2inds  24477  wlklenvm1  24532  wlkiswwlksur  24719  wwlknextbi  24725  wwlkextproplem2  24742  clwlkisclwwlklem1  24787  clwwisshclww  24807  erclwwlktr  24815  erclwwlkntr  24827  clwlkfclwwlk1hash  24842  vdgr1a  24906  vdusgra0nedg  24908  usgravd0nedg  24918  0eusgraiff0rgra  24939  rusgraprop2  24942  eupap1  24976  vdn0frgrav2  25023  vdgn0frgrav2  25024  ismndo2  25347  ghgrplem1OLD  25368  nvmul0or  25547  ipasslem5  25750  ipasslem11  25755  hvmul0or  25942  his6  26016  hhssnv  26180  ocsh  26201  ocin  26214  shsidmi  26302  chnlen0  26362  h1de2bi  26472  h1de2ctlem  26473  h1de2ci  26474  spansni  26475  3oalem1  26580  nmcexi  26945  atcveq0  27267  chcv1  27274  cdjreui  27351  cdj3lem2b  27356  xrge0tsmsd  27775  ordtrest2NEWlem  27904  ordtrest2NEW  27905  xrge0iifcnv  27915  esumc  28062  esumpcvgval  28084  ballotlemfc0  28431  ballotlemfcc  28432  dmgmaddn0  28565  subfacp1lem4  28627  subfacp1lem5  28628  erdszelem8  28642  sconpi1  28684  cvmsss2  28719  cvmlift2lem12  28759  msubco  28891  msubvrs  28920  sinccvglem  29038  untsucf  29082  dfpo2  29184  dfrdg2  29228  trpred0  29319  wfrlem10  29352  wfrlem14  29356  wfrlem15  29357  frrlem4  29390  colineardim1  29711  btwnconn1lem14  29750  segleantisym  29765  colinbtwnle  29768  outsidele  29782  lineunray  29797  linethru  29803  supaddc  30041  supadd  30042  itg2addnclem3  30068  ftc1anclem6  30095  dvasin  30103  elicc3  30135  opnregcld  30148  cldregopn  30149  fnejoin2  30187  unirep  30203  sdclem2  30235  ssbnd  30284  prdsbnd  30289  cntotbnd  30292  heibor1lem  30305  rrnequiv  30331  grpoeqdivid  30343  isdrngo3  30362  crngohomfo  30403  0idl  30422  1idl  30423  divrngidl  30425  smprngopr  30449  prnc  30464  ispridlc  30467  elrfi  30626  mrefg2  30639  eldiophb  30690  eldioph2b  30696  diophin  30706  diophun  30707  rexzrexnn0  30737  eldioph4b  30745  diophren  30747  rencldnfilem  30754  pellexlem6  30770  jm2.19  30935  rmydioph  30956  expdiophlem1  30963  expdioph  30965  lnr2i  31065  lpirlnr  31066  hbtlem2  31073  hbtlem4  31075  hbtlem6  31078  dgrsub2  31084  dgraa0p  31098  rngunsnply  31122  hashgcdlem  31157  radcnvrat  31195  lcmgcdeq  31216  pm14.24  31339  addrcom  31384  prodsnf  31587  afveu  32238  dfafn5b  32246  rlimdmafv  32262  uhgrauhg  32373  lincellss  33027  lindsrng01  33069  bnj145OLD  33782  riotaclbgBAD  34685  lshpdisj  34712  lsateln0  34720  lsatcveq0  34757  opnlen0  34913  cmtbr4N  34980  cvrnbtwn2  35000  cvrnbtwn4  35004  atcvreq0  35039  cvlatexch1  35061  exatleN  35128  atlelt  35162  ps-2  35202  llnn0  35240  lplnn0N  35271  islpln2a  35272  lvoln0N  35315  islvol2aN  35316  4at  35337  dalemcea  35384  dalem3  35388  pmapglb2N  35495  pmapglb2xN  35496  cdlema1N  35515  cdlemb  35518  paddasslem17  35560  llnexchb2lem  35592  llnexchb2  35593  lhpat3  35770  ltrnid  35859  trlne  35910  cdlemc4  35919  cdleme11h  35991  cdlemednuN  36025  cdlemg1a  36296  tendoeq2  36500  tendoid0  36551  dva1dim  36711  dib1dim  36892  dihlatat  37064  dochkrshp4  37116  dochkr1  37205  lclkrlem2e  37238  lcfrlem16  37285  lcfrlem28  37297  mapd0  37392  hdmap14lem13  37610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator