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

Theorem syl5ibrcom 235
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 234 . 2 (𝜒 → (𝜑𝜓))
43com12 32 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  biimprcd  238  elsn2g  4156  preq1b  4312  elpreqprb  4330  reusv2lem2OLD  4791  reusv3  4797  alxfr  4799  reuhypd  4816  opth1  4864  euotd  4891  otiunsndisj  4896  tz7.2  5012  frsn  5102  elsnxp  5580  ordtri1  5659  ordtri3  5662  fvmptdv2  6191  fveqressseq  6248  foco2  6272  foco2OLD  6273  fsn  6293  fnsnb  6315  fmptsng  6317  fmptsnd  6318  fconst2g  6351  fnprb  6355  fntpb  6356  funfvima  6374  soisoi  6456  isores3  6463  eusvobj2  6520  ovmpt2dv2  6670  f1opw2  6763  sorpssun  6819  sorpssin  6820  oneqmin  6874  nlimsucg  6911  onzsl  6915  tfinds  6928  funcnvuni  6989  opiota  7095  mpt2sn  7132  suppssov1  7191  suppssfv  7195  brtpos  7225  wfrlem10  7288  wfrlem14  7292  wfrlem15  7293  seqomlem1  7409  seqomlem2  7410  omordi  7510  omord  7512  omwordi  7515  oeeui  7546  nnmordi  7575  nnmord  7576  nnmwordi  7579  nnawordex  7581  nnaordex  7582  nneob  7596  omsmolem  7597  qsss  7672  eroveu  7706  mapsncnv  7767  ralxpmap  7770  elixpsn  7810  ixpsnf1o  7811  boxcutc  7814  pw2f1olem  7926  2pwne  7978  mapxpen  7988  mapunen  7991  php  8006  unxpdomlem2  8027  en1eqsnbi  8053  isfiniteg  8082  fofinf1o  8103  f1opwfi  8130  elfiun  8196  oieu  8304  brwdom2  8338  wdomtr  8340  ixpiunwdom  8356  en3lplem1  8371  suc11reg  8376  inf3lemd  8384  cantnfvalf  8422  cantnflt  8429  cantnfp1lem3  8437  cantnflem2  8447  r1tr  8499  dfac8alem  8712  wdomnumr  8747  isinfcard  8775  aceq3lem  8803  dfac5lem4  8809  dfac5  8811  dfac2  8813  coftr  8955  fin23lem28  9022  fin23lem29  9023  fin1a2lem11  9092  fin1a2lem12  9093  fin1a2lem13  9094  hsmexlem9  9107  axdclem  9201  pwcfsdom  9261  gchdomtri  9307  fpwwe2  9321  gchpwdom  9348  gchhar  9357  addnidpi  9579  nqereu  9607  genpv  9677  genpdm  9680  distrlem5pr  9705  mulid1  9893  ltne  9985  mul02  10065  cnegex  10068  mul0or  10516  negfi  10820  sup2  10828  supaddc  10837  supadd  10838  supmul1  10839  supmul  10842  creur  10861  creui  10862  cju  10863  nnsub  10906  un0addcl  11173  un0mulcl  11174  nn0sub  11190  elz2  11227  zaddcl  11250  suprzcl2  11610  qmulz  11623  qre  11625  qnegcl  11637  xrmax1  11839  xrmin2  11842  max1ALT  11850  xlesubadd  11922  xmulass  11946  xlemul1a  11947  xrsupexmnf  11963  xrinfmexpnf  11964  xrub  11970  iccid  12047  fzsn  12209  fzsuc2  12223  fz1sbc  12240  elfzp12  12243  modmuladd  12529  seqid3  12662  bcval5  12922  bcpasc  12925  hashbnd  12940  hashnnn0genn0  12945  hashprg  12995  hashprgOLD  12996  hashfzo  13028  wrdl1s1  13193  cats1un  13273  shftlem  13602  replim  13650  absmod0  13837  absz  13845  rlimdm  14076  summolem2  14240  summo  14241  zsum  14242  fsum  14244  fsummulc2  14304  fsumconst  14310  fsum00  14317  incexclem  14353  isumsplit  14357  infcvgaux1i  14374  prodmolem2  14450  prodmo  14451  zprod  14452  fprod  14456  prodsn  14477  prodsnf  14479  fprodconst  14493  ruclem2  14746  fzo0dvdseq  14829  bitsf1ocnv  14950  sadcaddlem  14963  smueqlem  14996  gcdabs1  15035  bezoutlem1  15040  bezoutlem3  15042  bezoutlem4  15043  dvdsgcd  15045  dvdsmulgcd  15058  lcmgcdeq  15109  lcmf  15130  lcmfunsnlem1  15134  lcmfunsnlem2lem2  15136  dvdsprime  15184  isprm5  15203  coprm  15207  prmdvdsexpr  15213  rpexp  15216  phibndlem  15259  dfphi2  15263  hashgcdlem  15277  odzdvds  15284  nnoddn2prm  15300  pythagtriplem1  15305  iserodd  15324  pceulem  15334  pcqmul  15342  pcqcl  15345  pcxcl  15349  pcneg  15362  pcabs  15363  pcgcd1  15365  pcz  15369  pcprmpw2  15370  pcprmpw  15371  dvdsprmpweqle  15374  difsqpwdvds  15375  pcaddlem  15376  pcadd  15377  pcmpt  15380  pockthg  15394  prmreclem5  15408  4sqlem4  15440  mul4sq  15442  vdwapun  15462  vdwlem2  15470  vdwlem6  15474  vdwlem8  15476  vdwlem13  15481  0ram  15508  ram0  15510  ramcl  15517  cshwsiun  15590  wunress  15713  firest  15862  xpscfv  15991  isssc  16249  pospo  16742  latnlej  16837  gsumval2a  17048  mnd1id  17101  mulgnn0p1  17321  mulgnn0ass  17347  gicsubgen  17490  symg1bas  17585  psgnunilem1  17682  psgnunilem2  17684  mndodcongi  17731  oddvdsnn0  17732  odnncl  17733  oddvds  17735  odeq  17738  odeq1  17746  pgpfi2  17790  sylow2a  17803  sylow2blem3  17806  sylow3lem6  17816  lsmelvalm  17835  lsmsubm  17837  lsmsubg  17838  lsmmod  17857  lsmdisj2  17864  efgmnvl  17896  efgtlen  17908  efgs1b  17918  efgrelexlemb  17932  efgredeu  17934  efgcpbllemb  17937  frgpuptinv  17953  frgpup3lem  17959  qusabl  18037  frgpnabllem1  18045  cyggeninv  18054  cyggenod  18055  cygabl  18061  gsumval3eu  18074  dprdssv  18184  dprdfeq0  18190  dprdsubg  18192  dprddisj2  18207  ablfacrp  18234  pgpfac1lem3  18245  pgpfaclem2  18250  dvreq1  18462  irredn1  18475  drngmul0or  18537  isabvd  18589  abvdom  18607  issrngd  18630  lmodfopnelem2  18669  lss1d  18730  lspsneq0  18779  lbspss  18849  lsmcl  18850  lvecvs0or  18875  lspindpi  18899  lidl1el  18985  lpiss  19017  lidldvgen  19022  nzrunit  19034  rrgeq0  19057  domneq0  19064  mplsubrglem  19206  mplmonmul  19231  mplcoe5lem  19234  coe1tmmul2  19413  coe1tmmul  19414  pf1ind  19486  qsssubdrg  19570  zringlpirlem1  19597  znfld  19673  znunit  19676  znrrg  19678  cygznlem3  19682  frgpcyg  19686  psgnghm  19690  ipeq0  19747  cssincl  19793  lsmcss  19797  obselocv  19833  dsmmacl  19846  dsmmlss  19849  mat1dimelbas  20038  mdetralt  20175  mdetunilem2  20180  mdetunilem7  20185  mdetunilem9  20187  maducoeval2  20207  chpscmat  20408  chfacfscmulgsum  20426  chfacfpmmulgsum  20430  istopon  20482  eltg3  20519  tgidm  20537  clsval2  20606  opncldf1  20640  restbas  20714  tgrest  20715  restcld  20728  restcldr  20730  restcls  20737  restntr  20738  ordtbas2  20747  ordtbas  20748  ordtrest2lem  20759  ordtrest2  20760  pnfnei  20776  mnfnei  20777  tgcn  20808  cnconst  20840  cnindis  20848  lmss  20854  ordtt1  20935  discmp  20953  1stcrest  21008  2ndcdisj  21011  cldllycmp  21050  txbas  21122  ptpjpre1  21126  ptuni2  21131  ptbasin  21132  ptbasfi  21136  ptopn2  21139  txbasval  21161  ptpjopn  21167  ptclsg  21170  dfac14lem  21172  xkoccn  21174  ptcnp  21177  upxp  21178  ptrescn  21194  txkgen  21207  xkoptsub  21209  xkopt  21210  xkoco1cn  21212  xkoco2cn  21213  xkococn  21215  xkoinjcn  21242  ordthmeolem  21356  ptuncnv  21362  nrmhaus  21381  fbssint  21394  fbfinnfr  21397  fbasrn  21440  isufil2  21464  filufint  21476  rnelfm  21509  fmfnfmlem2  21511  fmfnfmlem3  21512  fmfnfmlem4  21513  fmfnfm  21514  flimtopon  21526  flimclslem  21540  fclstopon  21568  fclscf  21581  flimfnfcls  21584  alexsublem  21600  alexsubALTlem3  21605  alexsubALTlem4  21606  ptcmplem2  21609  tmdgsum2  21652  symgtgp  21657  cldsubg  21666  qustgplem  21676  tgptsmscld  21706  tsmsxplem1  21708  imasdsf1olem  21929  blssps  21980  blss  21981  stdbdxmet  22071  methaus  22076  metrest  22080  nrginvrcn  22239  nmoeq0  22282  blssioo  22338  xrtgioo  22349  xrsxmet  22352  reconnlem1  22369  reconnlem2  22370  xrge0tsms  22377  elcncf1di  22437  iccpnfcnv  22482  evth  22497  lebnumlem1  22499  lebnumlem2  22500  lebnumlem3  22501  nmoleub3  22658  minveclem3b  22924  ivthlem2  22945  ivthlem3  22946  elovolm  22967  ovolmge0  22969  ovoliun  22997  ovolicc2lem3  23011  ovolicc2  23014  voliunlem3  23044  dyaddisj  23087  dyadmax  23089  opnmblALT  23094  ismbfd  23130  ismbf2d  23131  mbfimaopnlem  23145  mbfimaopn2  23147  i1fmullem  23184  i1fres  23195  itg1climres  23204  mbfi1fseqlem4  23208  itg2lcl  23217  itgsplitioo  23327  ellimc2  23364  rolle  23474  dvlip  23477  dvge0  23490  dvne0  23495  lhop1lem  23497  tdeglem4  23541  degltlem1  23553  deg1nn0clb  23571  deg1lt0  23572  dvdsq1p  23641  ply1rem  23644  fta1g  23648  elply2  23673  plyf  23675  ne0p  23684  plyeq0lem  23687  plypf1  23689  0dgrb  23723  coe1termlem  23735  dgrcolem2  23751  plymul0or  23757  plyrem  23781  fta1  23784  quotcan  23785  aalioulem3  23810  eff1olem  24015  lognegb  24057  eflogeq  24069  argregt0  24077  argrege0  24078  tanarg  24086  cxpexp  24131  cxpeq0  24141  mulcxp  24148  cxpeq  24215  atans2  24375  scvxcvx  24429  dmgmaddn0  24466  isppw2  24558  vmappw  24559  vmacl  24561  efvmacl  24563  isnsqf  24578  mumullem2  24623  sqff1o  24625  dvdsppwf1o  24629  ppiublem1  24644  vmalelog  24647  chtublem  24653  fsumvma  24655  perfectlem2  24672  perfect  24673  bposlem1  24726  lgsmod  24765  lgsne0  24777  lgsdirnn0  24786  lgsqr  24793  lgsdchr  24797  gausslemma2dlem1a  24807  gausslemma2dlem6  24814  lgseisenlem2  24818  lgsquadlem1  24822  lgsquadlem2  24823  2lgslem1b  24834  2sqlem2  24860  mul2sq  24861  2sqlem7  24866  dchrisum0fno1  24917  pntrsumbnd2  24973  ostthlem1  25033  ostth2lem2  25040  ostth3  25044  ostth  25045  colinearalg  25508  axpasch  25539  axlowdimlem16  25555  axlowdimlem17  25556  axlowdim  25559  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  usgraexmplef  25695  nbgraf1olem1  25736  nbgraf1olem3  25738  nbgraf1olem5  25740  nb3graprlem2  25747  cusgrasize2inds  25771  wlklenvm1  25826  wlkiswwlksur  26013  wwlknextbi  26019  wwlkextproplem2  26036  clwlkisclwwlklem1  26081  clwwisshclww  26101  erclwwlktr  26109  erclwwlkntr  26121  clwlkfclwwlk1hash  26135  vdgr1a  26199  vdusgra0nedg  26201  usgravd0nedg  26211  0eusgraiff0rgra  26232  rusgraprop2  26235  eupap1  26269  vdn0frgrav2  26316  vdgn0frgrav2  26317  nvmul0or  26677  ipasslem5  26880  ipasslem11  26885  hvmul0or  27072  his6  27146  hhssnv  27311  ocsh  27332  ocin  27345  shsidmi  27433  chnlen0  27493  h1de2bi  27603  h1de2ctlem  27604  h1de2ci  27605  spansni  27606  3oalem1  27711  nmcexi  28075  atcveq0  28397  chcv1  28404  cdjreui  28481  cdj3lem2b  28486  xrge0tsmsd  28922  ordtrest2NEWlem  29102  ordtrest2NEW  29103  xrge0iifcnv  29113  esumc  29246  esumpcvgval  29273  ballotlemfc0  29687  ballotlemfcc  29688  bnj145OLD  29855  subfacp1lem4  30225  subfacp1lem5  30226  erdszelem8  30240  sconpi1  30281  cvmsss2  30316  cvmlift2lem12  30356  msubco  30488  msubvrs  30517  sinccvglem  30626  untsucf  30647  dfpo2  30704  dfrdg2  30751  trpred0  30786  frrlem4  30833  colineardim1  31144  btwnconn1lem14  31183  segleantisym  31198  colinbtwnle  31201  outsidele  31215  lineunray  31230  linethru  31236  elicc3  31287  opnregcld  31301  cldregopn  31302  fnejoin2  31340  dissneqlem  32159  icorempt2  32171  relowlssretop  32183  relowlpssretop  32184  finxpsuclem  32206  lindsenlbs  32370  ptrecube  32375  poimirlem6  32381  poimirlem7  32382  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem21  32396  poimirlem22  32397  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  poimirlem29  32404  poimirlem30  32405  poimirlem31  32406  poimirlem32  32407  itg2addnclem3  32429  ftc1anclem6  32456  dvasin  32462  unirep  32473  sdclem2  32504  ssbnd  32553  prdsbnd  32558  cntotbnd  32561  heibor1lem  32574  rrnequiv  32600  ismndo2  32639  grpoeqdivid  32646  isdrngo3  32724  crngohomfo  32771  0idl  32790  1idl  32791  divrngidl  32793  smprngopr  32817  prnc  32832  ispridlc  32835  riotaclbgBAD  33054  lshpdisj  33088  lsateln0  33096  lsatcveq0  33133  opnlen0  33289  cmtbr4N  33356  cvrnbtwn2  33376  cvrnbtwn4  33380  atcvreq0  33415  cvlatexch1  33437  exatleN  33504  atlelt  33538  ps-2  33578  llnn0  33616  lplnn0N  33647  islpln2a  33648  lvoln0N  33691  islvol2aN  33692  4at  33713  dalemcea  33760  dalem3  33764  pmapglb2N  33871  pmapglb2xN  33872  cdlema1N  33891  cdlemb  33894  paddasslem17  33936  llnexchb2lem  33968  llnexchb2  33969  lhpat3  34146  ltrnid  34235  trlne  34286  cdlemc4  34295  cdleme11h  34367  cdlemednuN  34401  cdlemg1a  34672  tendoeq2  34876  tendoid0  34927  dva1dim  35087  dib1dim  35268  dihlatat  35440  dochkrshp4  35492  dochkr1  35581  lclkrlem2e  35614  lcfrlem16  35661  lcfrlem28  35673  mapd0  35768  hdmap14lem13  35986  elrfi  36071  mrefg2  36084  eldiophb  36134  eldioph2b  36140  diophin  36150  diophun  36151  rexzrexnn0  36182  eldioph4b  36189  diophren  36191  rencldnfilem  36198  pellexlem6  36212  jm2.19  36374  rmydioph  36395  expdiophlem1  36402  expdioph  36404  lnr2i  36501  lpirlnr  36502  hbtlem2  36509  hbtlem4  36511  hbtlem6  36514  dgrsub2  36520  dgraa0p  36534  rngunsnply  36558  radcnvrat  37331  pm14.24  37451  addrcom  37496  afveu  39680  dfafn5b  39688  rlimdmafv  39704  el1fzopredsuc  39746  fmtnofac2lem  39816  proththdlem  39866  perfectALTVlem2  39963  perfectALTV  39964  gbopos  39979  gbogt5  39982  gboage9  39984  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  riotaeqimp  40158  lpvtx  40285  uhgrauhgr  40288  usgredgop  40395  uhgrspansubgrlem  40509  uhgrspan1  40522  nbusgredgeu0  40591  nb3grprlem2  40604  cusgrsize2inds  40664  vtxd0nedgb  40698  rusgrpropnb  40778  upgr1wlkvtxedg  40848  1wlkp1lem1  40877  1wlkp1lem6  40882  1wlkp1lem8  40884  usgr2wlkneq  40957  crctcsh1wlk  41020  crctcsh  41022  1wlkiswwlks1  41059  wlkwwlksur  41089  wwlksnextbi  41095  wwlksnextproplem2  41111  wspthsnonn0vne  41119  clwlkclwwlklem2  41204  clwwlksext2edg  41225  clwwisshclwws  41230  erclwwlkstr  41238  erclwwlksntr  41250  clwlksfclwwlk1hash  41262  0wlkOns1  41284  31wlkdlem6  41327  eupth2eucrct  41380  lincellss  42004  lindsrng01  42046  suppdm  42089  nnpw2pb  42174
  Copyright terms: Public domain W3C validator