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

Theorem syl5ibcom 236
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1 (𝜑𝜓)
syl5ib.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5ibcom (𝜑 → (𝜒𝜃))

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3 (𝜑𝜓)
2 syl5ib.2 . . 3 (𝜒 → (𝜓𝜃))
31, 2syl5ib 235 . 2 (𝜒 → (𝜑𝜃))
43com12 32 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  biimpcd  240  elrab3t  3558  mob2  3584  rmob  3724  sneqrg  4558  preq1b  4565  prel12g  4586  disjxun  4842  sotric  5258  sotrieq  5259  iss  5652  poirr2  5731  xp11  5780  nordeq  5955  nsuceq0  6017  ordequn  6037  tz6.12c  6429  fnbrfvb  6452  foeqcnvco  6775  f1eqcocnv  6776  dfwe2  7207  mpt2sn  7498  tfrlem15  7720  tz7.44-2  7735  tz7.48-1  7770  tz7.49  7772  oawordexr  7869  oewordi  7904  oeeulem  7914  nna0r  7922  nnawordex  7950  nnaordex  7951  oaabs  7957  oaabs2  7958  ectocld  8045  ecoptocl  8068  mapsnd  8130  eqeng  8222  difsnen  8277  fopwdom  8303  frfi  8440  elfiun  8571  ordiso  8656  ordtypelem7  8664  wemaplem2  8687  suc11reg  8759  inf3lem6  8773  noinfep  8800  cantnff  8814  cantnfp1lem2  8819  cantnfp1lem3  8820  cantnflem1  8829  cantnf  8833  r111  8881  rankc2  8977  tcrank  8990  cardnueq0  9069  fodomfi2  9162  alephinit  9197  dfac9  9239  dfac12k  9250  cdainf  9295  ackbij1  9341  ackbij2  9346  sornom  9380  fin23lem16  9438  fin23lem21  9442  isf32lem2  9457  fin1a2lem6  9508  itunitc  9524  zorn2lem4  9602  wunr1om  9822  tskr1om  9870  recmulnq  10067  ltexnq  10078  distrlem4pr  10129  1re  10321  0re  10323  0cnALT  10551  mulge0  10827  prodgt0  11149  peano2nn  11313  recnz  11714  zneo  11722  uzn0  11916  xlemul1a  12332  prunioo  12520  flidz  12831  ceilidz  12871  modid2  12917  modmuladdnn0  12934  om2uzrani  12971  uzrdgfni  12977  seqid  13065  seqz  13068  facdiv  13290  facwordi  13292  hashdom  13382  wrdnval  13542  wrdl1s1  13605  sqrmo  14211  fsumf1o  14673  isumltss  14798  supcvg  14806  dvdsnegb  15218  odd2np1lem  15280  odd2np1  15281  ltoddhalfle  15301  halfleoddlt  15302  opoe  15303  omoe  15304  opeo  15305  omeo  15306  bitsuz  15411  bezoutlem4  15474  gcddiv  15483  gcdzeq  15486  dvdssqim  15488  lcmgcdeq  15540  coprmdvds2  15582  rpmul  15587  divgcdcoprmex  15594  cncongr2  15596  dvdsprm  15628  coprm  15636  prmdvdsexp  15640  prmdiv  15703  pythagtriplem19  15751  pc2dvds  15796  pcadd  15806  prmpwdvds  15821  vdwlem11  15908  ramubcl  15935  0ram  15937  posasymb  17153  pleval2  17166  pltval3  17168  plttr  17171  pospo  17174  letsr  17428  intopsn  17454  ismgmid  17465  imasmnd2  17528  isgrpid2  17659  isgrpinv  17673  dfgrp3lem  17714  imasgrp2  17731  orbsta  17943  symgfix2  18033  pmtrfrn  18075  pmtrrn2  18077  odmulg  18170  odmulgeq  18171  gexdvdsi  18195  gexnnod  18200  pgpssslw  18226  sylow2alem1  18229  fislw  18237  lsmss1b  18277  lsmss2b  18279  efgrelexlemb  18360  torsubg  18454  ablfacrplem  18662  pgpfac1lem2  18672  pgpfac1lem3  18674  imasring  18817  dvdsrcl2  18848  dvdsrtr  18850  dvdsrmul1  18851  irredn0  18901  lspsneq0  19215  lmhmima  19250  lspsolv  19347  opsrtoslem2  19689  mpfind  19740  mpfpf1  19919  pf1mpf  19920  xrsdsreclblem  19996  dvdsrzring  20035  prmirredlem  20045  znunit  20115  pjdm2  20262  obselocv  20279  lindfrn  20367  cpmadugsumlemF  20891  baspartn  20969  bastop  20996  iscld3  21079  isopn3  21081  iscldtop  21110  ordtrest2lem  21218  2ndcredom  21464  2ndc1stc  21465  2ndcrest  21468  2ndcdisj  21470  2ndcsep  21473  kgenidm  21561  dfac14  21632  tx2ndc  21665  kqreglem1  21755  rnelfm  21967  fmfnfmlem2  21969  fmfnfmlem4  21971  fmfnfm  21972  flimtopon  21984  fclstopon  22026  xrsmopn  22825  icccmplem2  22836  reconnlem1  22839  iccpnfcnv  22953  cphsqrtcl2  23195  ivthlem3  23433  ivthicc  23438  ovolctb  23470  ioombl  23545  itgabs  23814  itgsplitioo  23817  dvlip  23969  c1liplem1  23972  c1lip1  23973  dvgt0lem1  23978  dvivthlem2  23985  dvne0  23987  lhop1lem  23989  lhop1  23990  lhop2  23991  lhop  23992  dvcvx  23996  itgsubstlem  24024  mdegnn0cl  24044  ig1peu  24144  elply2  24165  plypf1  24181  dgreq0  24234  aannenlem3  24298  abelthlem2  24399  lognegb  24549  eflogeq  24561  efopn  24617  cxpge0  24642  cxplea  24655  cxple2  24656  cxpcn3lem  24701  cxpaddlelem  24705  cxpaddle  24706  cxpeq  24711  asinsinb  24837  acoscosb  24838  atantanb  24864  leibpilem1  24880  wilthlem2  25008  sqf11  25078  sqff1o  25121  ppiublem1  25140  lgsdir  25270  lgsne0  25273  lgsquadlem3  25320  2sqblem  25369  dchrisum0flblem1  25410  ostth3  25540  ostth  25541  colinearalg  26003  axcontlem5  26061  axcontlem9  26065  uhgrn0  26175  upgrfn  26195  umgrfn  26207  uvtxnbgrvtx  26512  vtxduhgr0nedg  26615  pthdivtx  26852  iswwlksnx  26960  wpthswwlks2on  27101  clwwlkn  27170  clwlksf1clwwlklem1OLD  27238  eupth2lem2  27391  eupth2lem3lem6  27405  htthlem  28101  pjpreeq  28584  h1dn0  28738  spansneleqi  28755  rnbra  29293  dfpjop  29368  elpjrn  29376  stm1i  29429  mdbr2  29482  mdsl2i  29508  sumdmdlem  29604  dmdbr6ati  29609  ordtrest2NEWlem  30292  xrge0iifcnv  30303  eulerpartlemb  30754  erdszelem8  31501  cvmlift3lem4  31625  cvmlift3lem5  31626  mrsub0  31734  mrsubccat  31736  mrsubcn  31737  msubrn  31747  msrid  31763  elmthm  31794  dvdspw  31956  dfon2lem9  32014  poseq  32072  noseponlem  32136  nodenselem4  32156  nodenselem5  32157  nodenselem7  32159  nodenselem8  32160  nolt02o  32164  nosupbnd2lem1  32180  noetalem3  32184  slerec  32242  btwnconn1lem11  32523  broutsideof2  32548  opnbnd  32639  tailfb  32691  bj-ismooredr2  33374  cnfinltrel  33555  fin2so  33707  poimirlem9  33729  poimirlem17  33737  poimirlem26  33746  poimirlem27  33747  poimirlem31  33751  itgabsnc  33789  ftc2nc  33804  sdclem2  33847  subspopn  33857  equivtotbnd  33886  rngosn3  34032  igenval2  34174  isfldidl  34176  relcnveq3  34405  ecex2  34413  iss2  34423  elrelscnveq3  34552  lshpinN  34767  lsatcv0eq  34825  lsatcv1  34826  cvrnbtwn3  35054  cvrnbtwn4  35057  cvrcmp  35061  atnlt  35091  cvlexchb1  35108  2llnne2N  35186  atcvr0eq  35204  lnnat  35205  cvrat4  35221  ps-1  35255  3at  35268  llncmp  35300  llnnlt  35301  llncvrlpln2  35335  llncvrlpln  35336  lplncmp  35340  lplnnlt  35343  lplncvrlvol2  35393  lplncvrlvol  35394  lvolcmp  35395  lvolnltN  35396  dalempnes  35429  dalemqnet  35430  dalem-cly  35449  dalem44  35494  lncmp  35561  cdlemblem  35571  llnexch2N  35648  osumcllem4N  35737  pexmidlem1N  35748  lhp2atnle  35811  cdleme11dN  36040  cdleme20k  36097  cdleme21at  36106  cdleme21ct  36107  cdleme32e  36223  cdleme35f  36232  tendoex  36753  dochexmidlem1  37238  lcfrlem9  37328  mapd1o  37426  mapdindp3  37500  ismrc  37763  pellexlem1  37892  aomclem4  38125  dfac21  38134  lsmfgcl  38142  lmhmfgima  38152  dfacbasgrp  38176  hbtlem6  38197  fiuneneq  38273  stoweidlem27  40720  stoweidlem29  40722  tz6.12c-afv2  41828  dfatbrafv2b  41831  fnbrafv2b  41834  iccpartrn  41938  prmdvdsfmtnof1lem2  42069  mod42tp1mod8  42091  assintopass  42415
  Copyright terms: Public domain W3C validator