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

Theorem syl5ibcom 246
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 245 . 2 (𝜒 → (𝜑𝜃))
43com12 32 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  biimpcd  250  elrab3t  3676  mob2  3703  rmob  3871  sneqrg  4762  preq1b  4769  prel12g  4786  disjxun  5055  sotric  5494  sotrieq  5495  iss  5896  poirr2  5977  xp11  6025  nordeq  6203  nsuceq0  6264  ordequn  6284  tz6.12c  6688  fnbrfvb  6711  foeqcnvco  7047  f1eqcocnv  7048  dfwe2  7485  releldmdifi  7733  mposn  7787  tfrlem15  8017  tz7.44-2  8032  tz7.48-1  8068  tz7.49  8070  oawordexr  8171  oewordi  8206  oeeulem  8216  nna0r  8224  nnawordex  8252  nnaordex  8253  oaabs  8260  oaabs2  8261  ectocld  8353  ecoptocl  8376  mapsnd  8438  eqeng  8531  difsnen  8587  fopwdom  8613  frfi  8751  elfiun  8882  ordiso  8968  ordtypelem7  8976  wemaplem2  8999  suc11reg  9070  inf3lem6  9084  noinfep  9111  cantnff  9125  cantnfp1lem2  9130  cantnfp1lem3  9131  cantnflem1  9140  cantnf  9144  r111  9192  rankc2  9288  tcrank  9301  cardnueq0  9381  fodomfi2  9474  alephinit  9509  dfac9  9550  dfac12k  9561  djuinf  9602  ackbij1  9648  ackbij2  9653  sornom  9687  fin23lem16  9745  fin23lem21  9749  isf32lem2  9764  fin1a2lem6  9815  itunitc  9831  zorn2lem4  9909  wunr1om  10129  tskr1om  10177  recmulnq  10374  ltexnq  10385  distrlem4pr  10436  1re  10629  0re  10631  0cnALT  10862  0cnALT2  10863  mulge0  11146  prodgt0  11475  peano2nn  11638  recnz  12045  zneo  12053  uzn0  12248  xlemul1a  12669  prunioo  12855  flidz  13168  ceilidz  13208  modid2  13254  modmuladdnn0  13271  om2uzrani  13308  uzrdgfni  13314  seqid  13403  seqz  13406  facdiv  13635  facwordi  13637  hashdom  13728  wrdnval  13884  wrdnfi  13887  wrdl1s1  13956  sqrmo  14599  fsumf1o  15068  isumltss  15191  supcvg  15199  dvdsnegb  15615  odd2np1lem  15677  odd2np1  15678  ltoddhalfle  15698  halfleoddlt  15699  opoe  15700  omoe  15701  opeo  15702  omeo  15703  bitsuz  15811  bezoutlem4  15878  gcddiv  15887  gcdzeq  15890  dvdssqim  15892  lcmgcdeq  15944  coprmdvds2  15986  rpmul  15991  divgcdcoprmex  15998  cncongr2  16000  dvdsprm  16035  coprm  16043  prmdvdsexp  16047  prmdiv  16110  pythagtriplem19  16158  pc2dvds  16203  pcadd  16213  prmpwdvds  16228  vdwlem11  16315  ramubcl  16342  0ram  16344  posasymb  17550  pleval2  17563  pltval3  17565  plttr  17568  pospo  17571  letsr  17825  intopsn  17852  ismgmid  17863  imasmnd2  17936  isgrpid2  18078  isgrpinv  18094  dfgrp3lem  18135  imasgrp2  18152  orbsta  18381  symgfix2  18473  pmtrfrn  18515  pmtrrn2  18517  odmulg  18612  odmulgeq  18613  gexdvdsi  18637  gexnnod  18642  pgpssslw  18668  sylow2alem1  18671  fislw  18679  lsmss1b  18721  lsmss2b  18723  efgrelexlemb  18805  torsubg  18903  ablfacrplem  19116  pgpfac1lem2  19126  pgpfac1lem3  19128  ablsimpnosubgd  19155  imasring  19298  dvdsrcl2  19329  dvdsrtr  19331  dvdsrmul1  19332  irredn0  19382  lspsneq0  19713  lmhmima  19748  lspsolv  19844  opsrtoslem2  20193  mpfind  20248  mpfpf1  20442  pf1mpf  20443  xrsdsreclblem  20519  dvdsrzring  20558  prmirredlem  20568  znunit  20638  pjdm2  20783  obselocv  20800  lindfrn  20893  cpmadugsumlemF  21412  baspartn  21490  bastop  21517  iscld3  21600  isopn3  21602  iscldtop  21631  ordtrest2lem  21739  2ndcredom  21986  2ndc1stc  21987  2ndcrest  21990  2ndcdisj  21992  2ndcsep  21995  kgenidm  22083  dfac14  22154  tx2ndc  22187  kqreglem1  22277  rnelfm  22489  fmfnfmlem2  22491  fmfnfmlem4  22493  fmfnfm  22494  flimtopon  22506  fclstopon  22548  xrsmopn  23347  icccmplem2  23358  reconnlem1  23361  iccpnfcnv  23475  cphsqrtcl2  23717  ivthlem3  23981  ivthicc  23986  ovolctb  24018  ioombl  24093  itgabs  24362  itgsplitioo  24365  dvlip  24517  c1liplem1  24520  c1lip1  24521  dvgt0lem1  24526  dvivthlem2  24533  dvne0  24535  lhop1lem  24537  lhop1  24538  lhop2  24539  lhop  24540  dvcvx  24544  itgsubstlem  24572  mdegnn0cl  24592  ig1peu  24692  elply2  24713  plypf1  24729  dgreq0  24782  aannenlem3  24846  abelthlem2  24947  lognegb  25100  eflogeq  25112  efopn  25168  cxpge0  25193  cxplea  25206  cxple2  25207  cxpcn3lem  25255  cxpaddlelem  25259  cxpaddle  25260  cxpeq  25265  asinsinb  25402  acoscosb  25403  atantanb  25429  wilthlem2  25573  sqf11  25643  sqff1o  25686  ppiublem1  25705  lgsdir  25835  lgsne0  25838  lgsquadlem3  25885  2sqblem  25934  dchrisum0flblem1  26011  ostth3  26141  ostth  26142  colinearalg  26623  axcontlem5  26681  axcontlem9  26685  uhgrn0  26779  upgrfn  26799  umgrfn  26811  uvtxnbgrvtx  27102  vtxduhgr0nedg  27201  pthdivtx  27437  iswwlksnx  27545  wpthswwlks2on  27667  clwwlkn  27731  clwwlknonwwlknonb  27812  eupth2lem2  27925  eupth2lem3lem6  27939  htthlem  28621  pjpreeq  29102  h1dn0  29256  spansneleqi  29273  rnbra  29811  dfpjop  29886  elpjrn  29894  stm1i  29947  mdbr2  30000  mdsl2i  30026  sumdmdlem  30122  dmdbr6ati  30127  ordtrest2NEWlem  31064  xrge0iifcnv  31075  eulerpartlemb  31525  erdszelem8  32342  cvmlift3lem4  32466  cvmlift3lem5  32467  fmlasucdisj  32543  mrsub0  32660  mrsubccat  32662  mrsubcn  32663  msubrn  32673  msrid  32689  elmthm  32720  dvdspw  32879  dfon2lem9  32933  poseq  32992  noseponlem  33068  nodenselem4  33088  nodenselem5  33089  nodenselem7  33091  nodenselem8  33092  nolt02o  33096  nosupbnd2lem1  33112  noetalem3  33116  slerec  33174  btwnconn1lem11  33455  broutsideof2  33480  opnbnd  33570  tailfb  33622  bj-ideqg1  34348  fin2so  34760  lindsadd  34766  poimirlem9  34782  poimirlem17  34790  poimirlem26  34799  poimirlem27  34800  poimirlem31  34804  itgabsnc  34842  ftc2nc  34857  sdclem2  34898  subspopn  34908  equivtotbnd  34937  rngosn3  35083  igenval2  35225  isfldidl  35227  relcnveq3  35459  ecex2  35466  iss2  35482  elrelscnveq3  35611  lshpinN  36005  lsatcv0eq  36063  lsatcv1  36064  cvrnbtwn3  36292  cvrnbtwn4  36295  cvrcmp  36299  atnlt  36329  cvlexchb1  36346  2llnne2N  36424  atcvr0eq  36442  lnnat  36443  cvrat4  36459  ps-1  36493  3at  36506  llncmp  36538  llnnlt  36539  llncvrlpln2  36573  llncvrlpln  36574  lplncmp  36578  lplnnlt  36581  lplncvrlvol2  36631  lplncvrlvol  36632  lvolcmp  36633  lvolnltN  36634  dalempnes  36667  dalemqnet  36668  dalem-cly  36687  dalem44  36732  lncmp  36799  cdlemblem  36809  llnexch2N  36886  osumcllem4N  36975  pexmidlem1N  36986  lhp2atnle  37049  cdleme11dN  37278  cdleme20k  37335  cdleme21at  37344  cdleme21ct  37345  cdleme32e  37461  cdleme35f  37470  tendoex  37991  dochexmidlem1  38476  lcfrlem9  38566  mapd1o  38664  mapdindp3  38738  elre0re  39032  dvdsexpim  39059  ismrc  39176  pellexlem1  39304  aomclem4  39535  dfac21  39544  lsmfgcl  39552  lmhmfgima  39562  dfacbasgrp  39586  hbtlem6  39607  fiuneneq  39675  stoweidlem27  42189  stoweidlem29  42191  tz6.12c-afv2  43318  dfatbrafv2b  43321  fnbrafv2b  43324  iccpartrn  43467  prmdvdsfmtnof1lem2  43624  mod42tp1mod8  43644  assintopass  44049  rrxsphere  44663
  Copyright terms: Public domain W3C validator