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

Theorem syl5ibcom 248
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 247 . 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:  biimpcd  252  elrab3t  3627  mob2  3654  rmob  3819  sneqrg  4730  preq1b  4737  prel12g  4754  disjxun  5028  sotric  5465  sotrieq  5466  iss  5870  poirr2  5951  xp11  5999  nordeq  6178  nsuceq0  6239  ordequn  6259  tz6.12c  6670  fnbrfvb  6693  foeqcnvco  7034  f1eqcocnv  7035  f1eqcocnvOLD  7036  dfwe2  7476  releldmdifi  7726  mposn  7781  tfrlem15  8011  tz7.44-2  8026  tz7.48-1  8062  tz7.49  8064  oawordexr  8165  oewordi  8200  oeeulem  8210  nna0r  8218  nnawordex  8246  nnaordex  8247  oaabs  8254  oaabs2  8255  ectocld  8347  ecoptocl  8370  mapsnd  8433  eqeng  8526  difsnen  8582  fopwdom  8608  frfi  8747  elfiun  8878  ordiso  8964  ordtypelem7  8972  wemaplem2  8995  suc11reg  9066  inf3lem6  9080  noinfep  9107  cantnff  9121  cantnfp1lem2  9126  cantnfp1lem3  9127  cantnflem1  9136  cantnf  9140  r111  9188  rankc2  9284  tcrank  9297  cardnueq0  9377  fodomfi2  9471  alephinit  9506  dfac9  9547  dfac12k  9558  djuinf  9599  ackbij1  9649  ackbij2  9654  sornom  9688  fin23lem16  9746  fin23lem21  9750  isf32lem2  9765  fin1a2lem6  9816  itunitc  9832  zorn2lem4  9910  wunr1om  10130  tskr1om  10178  recmulnq  10375  ltexnq  10386  distrlem4pr  10437  1re  10630  0re  10632  0cnALT  10863  0cnALT2  10864  mulge0  11147  prodgt0  11476  peano2nn  11637  recnz  12045  zneo  12053  uzn0  12248  xlemul1a  12669  prunioo  12859  flidz  13175  ceilidz  13215  modid2  13261  modmuladdnn0  13278  om2uzrani  13315  uzrdgfni  13321  seqid  13411  seqz  13414  facdiv  13643  facwordi  13645  hashdom  13736  wrdnval  13888  wrdnfi  13891  wrdl1s1  13959  sqrmo  14603  fsumf1o  15072  isumltss  15195  supcvg  15203  dvdsnegb  15619  odd2np1lem  15681  odd2np1  15682  ltoddhalfle  15702  halfleoddlt  15703  opoe  15704  omoe  15705  opeo  15706  omeo  15707  bitsuz  15813  bezoutlem4  15880  gcddiv  15889  gcdzeq  15892  dvdssqim  15894  lcmgcdeq  15946  coprmdvds2  15988  rpmul  15993  divgcdcoprmex  16000  cncongr2  16002  dvdsprm  16037  coprm  16045  prmdvdsexp  16049  prmdiv  16112  pythagtriplem19  16160  pc2dvds  16205  pcadd  16215  prmpwdvds  16230  vdwlem11  16317  ramubcl  16344  0ram  16346  posasymb  17554  pleval2  17567  pltval3  17569  plttr  17572  pospo  17575  letsr  17829  intopsn  17856  ismgmid  17867  imasmnd2  17940  isgrpid2  18132  isgrpinv  18148  dfgrp3lem  18189  imasgrp2  18206  orbsta  18435  symgfix2  18536  pmtrfrn  18578  pmtrrn2  18580  odmulg  18675  odmulgeq  18676  gexdvdsi  18700  gexnnod  18705  pgpssslw  18731  sylow2alem1  18734  fislw  18742  lsmss1b  18784  lsmss2b  18786  efgrelexlemb  18868  torsubg  18967  ablfacrplem  19180  pgpfac1lem2  19190  pgpfac1lem3  19192  ablsimpnosubgd  19219  imasring  19365  dvdsrcl2  19396  dvdsrtr  19398  dvdsrmul1  19399  irredn0  19449  lspsneq0  19777  lmhmima  19812  lspsolv  19908  xrsdsreclblem  20137  dvdsrzring  20176  prmirredlem  20186  znunit  20255  pjdm2  20400  obselocv  20417  lindfrn  20510  opsrtoslem2  20724  mpfind  20779  mpfpf1  20975  pf1mpf  20976  cpmadugsumlemF  21481  baspartn  21559  bastop  21586  iscld3  21669  isopn3  21671  iscldtop  21700  ordtrest2lem  21808  2ndcredom  22055  2ndc1stc  22056  2ndcrest  22059  2ndcdisj  22061  2ndcsep  22064  kgenidm  22152  dfac14  22223  tx2ndc  22256  kqreglem1  22346  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  fmfnfm  22563  flimtopon  22575  fclstopon  22617  xrsmopn  23417  icccmplem2  23428  reconnlem1  23431  iccpnfcnv  23549  cphsqrtcl2  23791  ivthlem3  24057  ivthicc  24062  ovolctb  24094  ioombl  24169  itgabs  24438  itgsplitioo  24441  dvlip  24596  c1liplem1  24599  c1lip1  24600  dvgt0lem1  24605  dvivthlem2  24612  dvne0  24614  lhop1lem  24616  lhop1  24617  lhop2  24618  lhop  24619  dvcvx  24623  itgsubstlem  24651  mdegnn0cl  24672  ig1peu  24772  elply2  24793  plypf1  24809  dgreq0  24862  aannenlem3  24926  abelthlem2  25027  lognegb  25181  eflogeq  25193  efopn  25249  cxpge0  25274  cxplea  25287  cxple2  25288  cxpcn3lem  25336  cxpaddlelem  25340  cxpaddle  25341  cxpeq  25346  asinsinb  25483  acoscosb  25484  atantanb  25510  wilthlem2  25654  sqf11  25724  sqff1o  25767  ppiublem1  25786  lgsdir  25916  lgsne0  25919  lgsquadlem3  25966  2sqblem  26015  dchrisum0flblem1  26092  ostth3  26222  ostth  26223  colinearalg  26704  axcontlem5  26762  axcontlem9  26766  uhgrn0  26860  upgrfn  26880  umgrfn  26892  uvtxnbgrvtx  27183  vtxduhgr0nedg  27282  pthdivtx  27518  iswwlksnx  27626  wpthswwlks2on  27747  clwwlkn  27811  clwwlknonwwlknonb  27891  eupth2lem2  28004  eupth2lem3lem6  28018  htthlem  28700  pjpreeq  29181  h1dn0  29335  spansneleqi  29352  rnbra  29890  dfpjop  29965  elpjrn  29973  stm1i  30026  mdbr2  30079  mdsl2i  30105  sumdmdlem  30201  dmdbr6ati  30206  ordtrest2NEWlem  31275  xrge0iifcnv  31286  eulerpartlemb  31736  erdszelem8  32558  cvmlift3lem4  32682  cvmlift3lem5  32683  fmlasucdisj  32759  mrsub0  32876  mrsubccat  32878  mrsubcn  32879  msubrn  32889  msrid  32905  elmthm  32936  dvdspw  33095  dfon2lem9  33149  poseq  33208  noseponlem  33284  nodenselem4  33304  nodenselem5  33305  nodenselem7  33307  nodenselem8  33308  nolt02o  33312  nosupbnd2lem1  33328  noetalem3  33332  slerec  33390  btwnconn1lem11  33671  broutsideof2  33696  opnbnd  33786  tailfb  33838  bj-ideqg1  34579  fin2so  35044  lindsadd  35050  poimirlem9  35066  poimirlem17  35074  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  itgabsnc  35126  ftc2nc  35139  sdclem2  35180  subspopn  35190  equivtotbnd  35216  rngosn3  35362  igenval2  35504  isfldidl  35506  relcnveq3  35738  ecex2  35745  iss2  35761  elrelscnveq3  35891  lshpinN  36285  lsatcv0eq  36343  lsatcv1  36344  cvrnbtwn3  36572  cvrnbtwn4  36575  cvrcmp  36579  atnlt  36609  cvlexchb1  36626  2llnne2N  36704  atcvr0eq  36722  lnnat  36723  cvrat4  36739  ps-1  36773  3at  36786  llncmp  36818  llnnlt  36819  llncvrlpln2  36853  llncvrlpln  36854  lplncmp  36858  lplnnlt  36861  lplncvrlvol2  36911  lplncvrlvol  36912  lvolcmp  36913  lvolnltN  36914  dalempnes  36947  dalemqnet  36948  dalem-cly  36967  dalem44  37012  lncmp  37079  cdlemblem  37089  llnexch2N  37166  osumcllem4N  37255  pexmidlem1N  37266  lhp2atnle  37329  cdleme11dN  37558  cdleme20k  37615  cdleme21at  37624  cdleme21ct  37625  cdleme32e  37741  cdleme35f  37750  tendoex  38271  dochexmidlem1  38756  lcfrlem9  38846  mapd1o  38944  mapdindp3  39018  elre0re  39460  dvdsexpim  39487  ismrc  39640  pellexlem1  39768  aomclem4  39999  dfac21  40008  lsmfgcl  40016  lmhmfgima  40026  dfacbasgrp  40050  hbtlem6  40071  fiuneneq  40139  stoweidlem27  42667  stoweidlem29  42669  tz6.12c-afv2  43796  dfatbrafv2b  43799  fnbrafv2b  43802  iccpartrn  43945  prmdvdsfmtnof1lem2  44100  mod42tp1mod8  44118  assintopass  44472  rrxsphere  45160
  Copyright terms: Public domain W3C validator