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

Theorem syl5ibrcom 250
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 249 . 2 (𝜒 → (𝜑𝜓))
43com12 32 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  biimprcd  253  elsn2g  4566  preq1b  4740  elpreqprb  4761  reusv3  5274  alxfr  5276  reuhypd  5288  opth1  5335  euotd  5371  otiunsndisj  5378  tz7.2  5507  frsn  5607  dmopab2rex  5754  elsnxp  6114  reuop  6116  ordtri1  6196  ordtri3  6199  fvmptdv2  6767  fveqressseq  6828  foco2  6854  fsn  6878  fnsnb  6909  fmptsng  6911  fmptsnd  6912  fconst2g  6946  fnprb  6952  fntpb  6953  funfvima  6974  soisoi  7064  isores3  7071  riotaeqimp  7123  eusvobj2  7132  ovmpodv2  7291  f1opw2  7384  sorpssun  7440  sorpssin  7441  oneqmin  7504  nlimsucg  7541  onzsl  7545  tfinds  7558  funcnvuni  7622  opiota  7743  mposn  7785  suppssov1  7849  suppssfv  7853  brtpos  7888  wfrlem10  7951  wfrlem14  7955  wfrlem15  7956  seqomlem1  8073  seqomlem2  8074  omordi  8179  omord  8181  omwordi  8184  oeeui  8215  nnmordi  8244  nnmord  8245  nnmwordi  8248  nnawordex  8250  nnaordex  8251  nneob  8266  omsmolem  8267  qsss  8345  eroveu  8379  mapsncnv  8444  ralxpmap  8447  elixpsn  8488  ixpsnf1o  8489  boxcutc  8492  pw2f1olem  8608  2pwne  8661  mapxpen  8671  mapunen  8674  php  8689  unxpdomlem2  8711  en1eqsnbi  8737  isfiniteg  8766  fofinf1o  8787  f1opwfi  8816  elfiun  8882  oieu  8991  brwdom2  9025  wdomtr  9027  ixpiunwdom  9042  en3lplem1  9063  suc11reg  9070  inf3lemd  9078  cantnfvalf  9116  cantnflt  9123  cantnfp1lem3  9131  cantnflem2  9141  r1tr  9193  updjud  9351  dfac8alem  9444  wdomnumr  9479  isinfcard  9507  aceq3lem  9535  dfac5lem4  9541  dfac5  9543  dfac2b  9545  coftr  9688  fin23lem28  9755  fin23lem29  9756  fin1a2lem11  9825  fin1a2lem12  9826  fin1a2lem13  9827  hsmexlem9  9840  axdclem  9934  pwcfsdom  9998  gchdomtri  10044  fpwwe2  10058  gchpwdom  10085  gchhar  10094  addnidpi  10316  nqereu  10344  genpv  10414  genpdm  10417  distrlem5pr  10442  mulid1  10632  ltne  10730  mul02  10811  cnegex  10814  mul0or  11273  negfi  11581  sup2  11588  supaddc  11599  supadd  11600  supmul1  11601  supmul  11604  creur  11623  creui  11624  cju  11625  nnsub  11673  un0addcl  11922  un0mulcl  11923  nn0sub  11939  elz2  11991  zaddcl  12014  suprzcl2  12330  qmulz  12343  qre  12345  qnegcl  12357  elpqb  12367  xrmax1  12560  xrmin2  12563  max1ALT  12571  xlesubadd  12648  xmulass  12672  xlemul1a  12673  xrsupexmnf  12690  xrinfmexpnf  12691  xrub  12697  iccid  12775  fzsn  12948  fzsuc2  12964  fz1sbc  12982  elfzp12  12985  modmuladd  13280  seqid3  13414  bcval5  13678  bcpasc  13681  hashbnd  13696  hashnnn0genn0  13703  hashprg  13756  hashfzo  13790  wrdl1s1  13963  ccats1alpha  13968  cats1un  14078  shftlem  14422  replim  14470  absmod0  14658  absz  14666  rlimdm  14903  summolem2  15068  summo  15069  zsum  15070  fsum  15072  fsummulc2  15134  fsumconst  15140  fsum00  15148  incexclem  15186  isumsplit  15190  infcvgaux1i  15207  prodmolem2  15284  prodmo  15285  zprod  15286  fprod  15290  prodsn  15311  prodsnf  15313  fprodconst  15327  ruclem2  15580  fzo0dvdseq  15668  bitsf1ocnv  15786  sadcaddlem  15799  smueqlem  15832  gcdabs1  15871  bezoutlem1  15880  bezoutlem3  15882  bezoutlem4  15883  dvdsgcd  15885  dvdsmulgcd  15898  lcmgcdeq  15949  lcmf  15970  lcmfunsnlem1  15974  lcmfunsnlem2lem2  15976  isprm2lem  16018  dvdsprime  16024  isprm5  16044  coprm  16048  prmdvdsexpr  16054  rpexp  16057  phibndlem  16100  dfphi2  16104  hashgcdlem  16118  odzdvds  16125  nnoddn2prm  16141  pythagtriplem1  16146  iserodd  16165  pceulem  16175  pcqmul  16183  pcqcl  16186  pcxcl  16190  pcneg  16203  pcabs  16204  pcgcd1  16206  pcz  16210  pcprmpw2  16211  pcprmpw  16212  dvdsprmpweqle  16215  difsqpwdvds  16216  pcaddlem  16217  pcadd  16218  pcmpt  16221  pockthg  16235  prmreclem5  16249  4sqlem4  16281  mul4sq  16283  vdwapun  16303  vdwlem2  16311  vdwlem6  16315  vdwlem8  16317  vdwlem13  16322  0ram  16349  ram0  16351  ramcl  16358  cshwsiun  16428  wunress  16559  firest  16701  isssc  17085  pospo  17578  latnlej  17673  gsumval2a  17890  mnd1id  17948  0subm  17977  mulgnn0p1  18234  mulgnn0ass  18258  cyccom  18341  gicsubgen  18413  symg1bas  18514  snsymgefmndeq  18518  psgnunilem1  18616  psgnunilem2  18618  mndodcongi  18666  oddvdsnn0  18667  odnncl  18668  oddvds  18670  odeq  18673  odeq1  18682  pgpfi2  18726  sylow2a  18739  sylow2blem3  18742  sylow3lem6  18752  lsmelvalm  18771  lsmsubm  18773  lsmsubg  18774  lsmmod  18796  lsmdisj2  18803  efgmnvl  18835  efgtlen  18847  efgs1b  18857  efgrelexlemb  18871  efgredeu  18873  efgcpbllemb  18876  frgpuptinv  18892  frgpup3lem  18898  qusabl  18981  frgpnabllem1  18989  cyggeninv  18998  cyggenod  18999  cygablOLD  19007  gsumval3eu  19020  dprdssv  19134  dprdfeq0  19140  dprdsubg  19142  dprddisj2  19157  ablfacrp  19184  pgpfac1lem3  19195  pgpfaclem2  19200  dvreq1  19442  irredn1  19455  drngmul0or  19519  isabvd  19587  abvdom  19605  issrngd  19628  lmodfopnelem2  19667  lss1d  19731  lspsneq0  19780  lbspss  19850  lsmcl  19851  lvecvs0or  19876  lspindpi  19900  lidl1el  19987  lpiss  20019  lidldvgen  20024  nzrunit  20036  rrgeq0  20059  domneq0  20066  qsssubdrg  20153  zringlpirlem1  20180  znfld  20255  znunit  20258  znrrg  20260  cygznlem3  20264  frgpcyg  20268  psgnghm  20272  ipeq0  20330  cssincl  20380  lsmcss  20384  obselocv  20420  dsmmacl  20433  dsmmlss  20436  mplsubrglem  20680  mplmonmul  20707  mplcoe5lem  20710  mhpvarcl  20801  coe1tmmul2  20908  coe1tmmul  20909  pf1ind  20982  mat1dimelbas  21079  mdetralt  21216  mdetunilem2  21221  mdetunilem7  21226  mdetunilem9  21228  maducoeval2  21248  chpscmat  21450  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  istopon  21520  eltg3  21570  tgidm  21588  clsval2  21658  opncldf1  21692  restbas  21766  tgrest  21767  restcld  21780  restcldr  21782  restcls  21789  restntr  21790  ordtbas2  21799  ordtbas  21800  ordtrest2lem  21811  ordtrest2  21812  pnfnei  21828  mnfnei  21829  tgcn  21860  cnconst  21892  cnindis  21900  lmss  21906  ordtt1  21987  discmp  22006  1stcrest  22061  2ndcdisj  22064  cldllycmp  22103  txbas  22175  ptpjpre1  22179  ptuni2  22184  ptbasin  22185  ptbasfi  22189  ptopn2  22192  txbasval  22214  ptpjopn  22220  ptclsg  22223  dfac14lem  22225  xkoccn  22227  ptcnp  22230  upxp  22231  ptrescn  22247  txkgen  22260  xkoptsub  22262  xkopt  22263  xkoco1cn  22265  xkoco2cn  22266  xkococn  22268  xkoinjcn  22295  ordthmeolem  22409  ptuncnv  22415  nrmhaus  22434  fbssint  22446  fbfinnfr  22449  fbasrn  22492  isufil2  22516  filufint  22528  rnelfm  22561  fmfnfmlem2  22563  fmfnfmlem3  22564  fmfnfmlem4  22565  fmfnfm  22566  flimtopon  22578  flimclslem  22592  fclstopon  22620  fclscf  22633  flimfnfcls  22636  alexsublem  22652  alexsubALTlem3  22657  alexsubALTlem4  22658  ptcmplem2  22661  tmdgsum2  22704  symgtgp  22714  cldsubg  22719  qustgplem  22729  tgptsmscld  22759  tsmsxplem1  22761  imasdsf1olem  22983  blssps  23034  blss  23035  stdbdxmet  23125  methaus  23130  metrest  23134  nrginvrcn  23301  nmoeq0  23345  blssioo  23403  xrtgioo  23414  xrsxmet  23417  reconnlem1  23434  reconnlem2  23435  xrge0tsms  23442  elcncf1di  23503  iccpnfcnv  23552  evth  23567  lebnumlem1  23569  lebnumlem2  23570  lebnumlem3  23571  nmoleub3  23727  minveclem3b  24035  ivthlem2  24059  ivthlem3  24060  elovolm  24082  ovolmge0  24084  ovoliun  24112  ovolicc2lem3  24126  ovolicc2  24129  voliunlem3  24159  dyaddisj  24203  dyadmax  24205  opnmblALT  24210  ismbfd  24246  ismbf2d  24247  mbfimaopnlem  24262  mbfimaopn2  24264  i1fmullem  24301  i1fres  24312  itg1climres  24321  mbfi1fseqlem4  24325  itg2lcl  24334  itgsplitioo  24444  ellimc2  24483  rolle  24596  dvlip  24599  dvge0  24612  dvne0  24617  lhop1lem  24619  tdeglem4  24664  degltlem1  24676  deg1nn0clb  24694  deg1lt0  24695  dvdsq1p  24764  ply1rem  24767  fta1g  24771  elply2  24796  plyf  24798  ne0p  24807  plyeq0lem  24810  plypf1  24812  0dgrb  24846  coe1termlem  24858  dgrcolem2  24874  plymul0or  24880  plyrem  24904  fta1  24907  quotcan  24908  aalioulem3  24933  eff1olem  25143  lognegb  25184  eflogeq  25196  argregt0  25204  argrege0  25205  tanarg  25213  cxpexp  25262  cxpeq0  25272  mulcxp  25279  cxpeq  25349  atans2  25520  scvxcvx  25574  dmgmaddn0  25611  isppw2  25703  vmappw  25704  vmacl  25706  efvmacl  25708  isnsqf  25723  mumullem2  25768  sqff1o  25770  dvdsppwf1o  25774  ppiublem1  25789  vmalelog  25792  chtublem  25798  fsumvma  25800  perfectlem2  25817  perfect  25818  bposlem1  25871  lgsmod  25910  lgsne0  25922  lgsdirnn0  25931  lgsqr  25938  lgsdchr  25942  gausslemma2dlem1a  25952  gausslemma2dlem6  25959  lgseisenlem2  25963  lgsquadlem1  25967  lgsquadlem2  25968  2lgslem1b  25979  2sqlem2  26005  mul2sq  26006  2sqlem7  26011  dchrisum0fno1  26098  pntrsumbnd2  26154  ostthlem1  26214  ostth2lem2  26221  ostth3  26225  ostth  26226  colinearalg  26707  axpasch  26738  axlowdimlem16  26754  axlowdimlem17  26755  axlowdim  26758  axcontlem2  26762  axcontlem4  26764  axcontlem7  26767  lpvtx  26864  edglnl  26939  numedglnl  26940  usgredgop  26966  usgrexmplef  27052  uhgrspansubgrlem  27083  uhgrspan1  27096  nbusgredgeu0  27161  nb3grprlem2  27174  cusgrsize2inds  27246  vtxd0nedgb  27281  rusgrpropnb  27376  upgrwlkvtxedg  27437  wlkp1lem1  27466  wlkp1lem6  27471  wlkp1lem8  27473  usgr2wlkneq  27548  crctcshwlk  27611  crctcsh  27613  iswwlksnon  27642  wlkiswwlks1  27656  wwlksnextbi  27683  wwlksnextproplem2  27699  wspthsnonn0vne  27706  clwlkclwwlklem2  27788  clwwisshclwws  27803  erclwwlktr  27810  clwwlkel  27834  clwwlkext2edg  27844  erclwwlkntr  27859  clwlknf1oclwwlknlem2  27870  clwlknf1oclwwlknlem3  27871  clwlknf1oclwwlkn  27872  clwwlknonccat  27884  0wlkons1  27909  3wlkdlem6  27953  eupth2eucrct  28005  frgrwopreglem2  28101  2clwwlk2clwwlk  28138  wlkl0  28155  nvmul0or  28436  ipasslem5  28621  ipasslem11  28626  hvmul0or  28811  his6  28885  hhssnv  29050  ocsh  29069  ocin  29082  shsidmi  29170  chnlen0  29230  h1de2bi  29340  h1de2ctlem  29341  h1de2ci  29342  spansni  29343  3oalem1  29448  nmcexi  29812  atcveq0  30134  chcv1  30141  cdjreui  30218  cdj3lem2b  30223  xrge0tsmsd  30745  ccfldextdgrr  31145  ordtrest2NEWlem  31273  ordtrest2NEW  31274  xrge0iifcnv  31284  esumc  31418  esumpcvgval  31445  ballotlemfc0  31858  ballotlemfcc  31859  subfacp1lem4  32538  subfacp1lem5  32539  erdszelem8  32553  sconnpi1  32594  cvmsss2  32629  cvmlift2lem12  32669  satfv0  32713  satfv0fun  32726  satf00  32729  sat1el2xp  32734  fmla0xp  32738  fmlasucdisj  32754  satffunlem1lem1  32757  satffunlem2lem1  32759  dmopab3rexdif  32760  msubco  32886  msubvrs  32915  sinccvglem  33023  untsucf  33044  dfpo2  33099  eqfunresadj  33112  dfrdg2  33148  trpred0  33183  frrlem12  33242  frrlem13  33243  nolesgn2ores  33287  nolt02o  33307  nosupbnd2  33324  noetalem3  33327  colineardim1  33630  btwnconn1lem14  33669  segleantisym  33684  colinbtwnle  33687  outsidele  33701  lineunray  33716  linethru  33722  elicc3  33773  opnregcld  33786  cldregopn  33787  fnejoin2  33825  dissneqlem  34752  icorempo  34763  relowlssretop  34775  relowlpssretop  34776  rdgssun  34790  finxpsuclem  34809  lindsenlbs  35045  ptrecube  35050  poimirlem6  35056  poimirlem7  35057  poimirlem16  35066  poimirlem17  35067  poimirlem19  35069  poimirlem20  35070  poimirlem21  35071  poimirlem22  35072  poimirlem23  35073  poimirlem24  35074  poimirlem25  35075  poimirlem26  35076  poimirlem27  35077  poimirlem29  35079  poimirlem30  35080  poimirlem31  35081  poimirlem32  35082  itg2addnclem3  35103  ftc1anclem6  35128  dvasin  35134  unirep  35144  sdclem2  35173  ssbnd  35219  prdsbnd  35224  cntotbnd  35227  heibor1lem  35240  rrnequiv  35266  ismndo2  35305  grpoeqdivid  35312  isdrngo3  35390  crngohomfo  35437  0idl  35456  1idl  35457  divrngidl  35459  smprngopr  35483  prnc  35498  ispridlc  35501  riotaclbgBAD  36243  lshpdisj  36276  lsateln0  36284  lsatcveq0  36321  opnlen0  36477  cmtbr4N  36544  cvrnbtwn2  36564  cvrnbtwn4  36568  atcvreq0  36603  cvlatexch1  36625  exatleN  36693  atlelt  36727  ps-2  36767  llnn0  36805  lplnn0N  36836  islpln2a  36837  lvoln0N  36880  islvol2aN  36881  4at  36902  dalemcea  36949  dalem3  36953  pmapglb2N  37060  pmapglb2xN  37061  cdlema1N  37080  cdlemb  37083  paddasslem17  37125  llnexchb2lem  37157  llnexchb2  37158  lhpat3  37335  ltrnid  37424  trlne  37474  cdlemc4  37483  cdleme11h  37555  cdlemednuN  37589  cdlemg1a  37859  tendoeq2  38063  tendoid0  38114  dva1dim  38274  dib1dim  38454  dihlatat  38626  dochkrshp4  38678  dochkr1  38767  lclkrlem2e  38800  lcfrlem16  38847  lcfrlem28  38859  mapd0  38954  hdmap14lem13  39169  fnsnbt  39401  frlmsnic  39440  reladdrsub  39510  sn-negex12  39540  sn-mulid2  39559  sn-mul02  39564  mulgt0con1d  39570  mulgt0con2d  39571  sn-sup2  39581  elrfi  39622  mrefg2  39635  eldiophb  39685  eldioph2b  39691  diophin  39700  diophun  39701  rexzrexnn0  39732  eldioph4b  39739  diophren  39741  rencldnfilem  39748  pellexlem6  39762  jm2.19  39921  rmydioph  39942  expdiophlem1  39949  expdioph  39951  lnr2i  40047  lpirlnr  40048  hbtlem2  40055  hbtlem4  40057  hbtlem6  40060  dgrsub2  40066  dgraa0p  40080  rngunsnply  40104  dfsucon  40218  radcnvrat  41005  pm14.24  41123  addrcom  41166  afveu  43696  dfafn5b  43704  rlimdmafv  43720  afv2eu  43781  rlimdmafv2  43801  el1fzopredsuc  43869  elsetpreimafvssdm  43890  imasetpreimafvbijlemfo  43909  sprvalpw  43984  prprvalpw  44019  reupr  44026  fmtnofac2lem  44072  proththdlem  44118  perfectALTVlem2  44227  perfectALTV  44228  gbowpos  44264  gbowgt5  44267  gboge9  44269  nnsum4primesodd  44301  nnsum4primesoddALTV  44302  isomuspgr  44339  lincellss  44822  lindsrng01  44864  suppdm  44906  nnpw2pb  44988  0aryfvalel  45035  0aryfvalelfv  45036  itsclc0xyqsolr  45170
  Copyright terms: Public domain W3C validator