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

Theorem syl5ibcom 235
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 234 . 2 (𝜒 → (𝜑𝜃))
43com12 32 1 (𝜑 → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  biimpcd  239  elrab3t  3350  mob2  3373  rmob  3515  sneqrg  4345  preq1b  4352  disjxun  4621  sotric  5031  sotrieq  5032  iss  5416  poirr2  5489  xp11  5538  nordeq  5711  nsuceq0  5774  suctrOLD  5778  ordequn  5797  tz6.12c  6180  fnbrfvb  6203  foeqcnvco  6520  f1eqcocnv  6521  dfwe2  6943  mpt2sn  7228  tfrlem15  7448  tz7.44-2  7463  tz7.48-1  7498  tz7.49  7500  oawordexr  7596  oewordi  7631  oeeulem  7641  nna0r  7649  nnawordex  7677  nnaordex  7678  oaabs  7684  oaabs2  7685  ectocld  7774  ecoptocl  7797  mapsn  7859  eqeng  7949  difsnen  8002  fopwdom  8028  frfi  8165  elfiun  8296  ordiso  8381  ordtypelem7  8389  wemaplem2  8412  suc11reg  8476  inf3lem6  8490  noinfep  8517  cantnff  8531  cantnfp1lem2  8536  cantnfp1lem3  8537  cantnflem1  8546  cantnf  8550  r111  8598  rankc2  8694  tcrank  8707  cardnueq0  8750  fodomfi2  8843  alephinit  8878  dfac9  8918  dfac12k  8929  cdainf  8974  ackbij1  9020  ackbij2  9025  sornom  9059  fin23lem16  9117  fin23lem21  9121  isf32lem2  9136  fin1a2lem6  9187  itunitc  9203  zorn2lem4  9281  wunr1om  9501  tskr1om  9549  recmulnq  9746  ltexnq  9757  distrlem4pr  9808  1re  9999  0re  10000  0cnALT  10230  mulge0  10506  prodgt0  10828  peano2nn  10992  recnz  11412  zneo  11420  uzn0  11663  xlemul1a  12077  prunioo  12259  flidz  12567  ceilidz  12607  modid2  12653  modmuladdnn0  12670  om2uzrani  12707  uzrdgfni  12713  seqid  12802  seqz  12805  facdiv  13030  facwordi  13032  hashdom  13124  wrdnval  13290  wrdl1s1  13349  sqrmo  13942  fsumf1o  14403  isumltss  14524  supcvg  14532  dvdsnegb  14942  odd2np1lem  15007  odd2np1  15008  ltoddhalfle  15028  halfleoddlt  15029  opoe  15030  omoe  15031  opeo  15032  omeo  15033  bitsuz  15139  bezoutlem4  15202  gcddiv  15211  gcdzeq  15214  dvdssqim  15216  lcmgcdeq  15268  coprmdvds2  15311  rpmul  15316  divgcdcoprmex  15323  cncongr2  15325  dvdsprm  15358  coprm  15366  prmdvdsexp  15370  prmdiv  15433  pythagtriplem19  15481  pc2dvds  15526  pcadd  15536  prmpwdvds  15551  vdwlem11  15638  ramubcl  15665  0ram  15667  mreexexdOLD  16249  posasymb  16892  pleval2  16905  pltval3  16907  plttr  16910  pospo  16913  letsr  17167  intopsn  17193  ismgmid  17204  imasmnd2  17267  isgrpid2  17398  isgrpinv  17412  dfgrp3lem  17453  imasgrp2  17470  orbsta  17686  symgfix2  17776  pmtrfrn  17818  pmtrrn2  17820  odmulg  17913  odmulgeq  17914  gexdvdsi  17938  gexnnod  17943  pgpssslw  17969  sylow2alem1  17972  fislw  17980  lsmss1b  18020  lsmss2b  18022  efgrelexlemb  18103  torsubg  18197  ablfacrplem  18404  pgpfac1lem2  18414  pgpfac1lem3  18416  imasring  18559  dvdsrcl2  18590  dvdsrtr  18592  dvdsrmul1  18593  irredn0  18643  lspsneq0  18952  lmhmima  18987  lspsolv  19083  opsrtoslem2  19425  mpfind  19476  mpfpf1  19655  pf1mpf  19656  xrsdsreclblem  19732  dvdsrzring  19771  prmirredlem  19781  znunit  19852  pjdm2  19995  obselocv  20012  lindfrn  20100  cpmadugsumlemF  20621  baspartn  20698  bastop  20725  iscld3  20808  isopn3  20810  iscldtop  20839  ordtrest2lem  20947  2ndcredom  21193  2ndc1stc  21194  2ndcrest  21197  2ndcdisj  21199  2ndcsep  21202  kgenidm  21290  dfac14  21361  tx2ndc  21394  kqreglem1  21484  rnelfm  21697  fmfnfmlem2  21699  fmfnfmlem4  21701  fmfnfm  21702  flimtopon  21714  fclstopon  21756  xrsmopn  22555  icccmplem2  22566  reconnlem1  22569  iccpnfcnv  22683  cphsqrtcl2  22926  ivthlem3  23162  ivthicc  23167  ovolctb  23198  ioombl  23273  itgabs  23541  itgsplitioo  23544  dvlip  23694  c1liplem1  23697  c1lip1  23698  dvgt0lem1  23703  dvivthlem2  23710  dvne0  23712  lhop1lem  23714  lhop1  23715  lhop2  23716  lhop  23717  dvcvx  23721  itgsubstlem  23749  mdegnn0cl  23769  ig1peu  23869  elply2  23890  plypf1  23906  dgreq0  23959  aannenlem3  24023  abelthlem2  24124  lognegb  24274  eflogeq  24286  efopn  24338  cxpge0  24363  cxplea  24376  cxple2  24377  cxpcn3lem  24422  cxpaddlelem  24426  cxpaddle  24427  cxpeq  24432  asinsinb  24558  acoscosb  24559  atantanb  24585  leibpilem1  24601  wilthlem2  24729  sqf11  24799  sqff1o  24842  ppiublem1  24861  lgsdir  24991  lgsne0  24994  lgsquadlem3  25041  2sqblem  25090  dchrisum0flblem1  25131  ostth3  25261  ostth  25262  colinearalg  25724  axcontlem5  25782  axcontlem9  25786  uhgrn0  25892  upgrfn  25912  umgrfn  25923  uspgrf1oedg  25995  uvtxanbgrvtx  26214  vtxduhgr0nedg  26308  pthdivtx  26528  iswwlksnx  26634  clwlksf1clwwlklem1  26865  eupth2lem2  26979  eupth2lem3lem6  26993  htthlem  27662  pjpreeq  28145  h1dn0  28299  spansneleqi  28316  rnbra  28854  dfpjop  28929  elpjrn  28937  stm1i  28990  mdbr2  29043  mdsl2i  29069  sumdmdlem  29165  dmdbr6ati  29170  ordtrest2NEWlem  29792  xrge0iifcnv  29803  eulerpartlemb  30253  erdszelem8  30941  cvmlift3lem4  31065  cvmlift3lem5  31066  mrsub0  31174  mrsubccat  31176  mrsubcn  31177  msubrn  31187  msrid  31203  elmthm  31234  dvdspw  31397  dfon2lem9  31450  poseq  31504  noseponlem  31575  nodenselem3  31599  nodenselem5  31601  nodenselem8  31604  btwnconn1lem11  31899  broutsideof2  31924  opnbnd  32015  tailfb  32067  fin2so  33067  poimirlem9  33089  poimirlem17  33097  poimirlem26  33106  poimirlem27  33107  poimirlem31  33111  itgabsnc  33150  ftc2nc  33165  sdclem2  33209  subspopn  33219  equivtotbnd  33248  rngosn3  33394  igenval2  33536  isfldidl  33538  lshpinN  33795  lsatcv0eq  33853  lsatcv1  33854  cvrnbtwn3  34082  cvrnbtwn4  34085  cvrcmp  34089  atnlt  34119  cvlexchb1  34136  2llnne2N  34213  atcvr0eq  34231  lnnat  34232  cvrat4  34248  ps-1  34282  3at  34295  llncmp  34327  llnnlt  34328  llncvrlpln2  34362  llncvrlpln  34363  lplncmp  34367  lplnnlt  34370  lplncvrlvol2  34420  lplncvrlvol  34421  lvolcmp  34422  lvolnltN  34423  dalempnes  34456  dalemqnet  34457  dalem-cly  34476  dalem44  34521  lncmp  34588  cdlemblem  34598  llnexch2N  34675  osumcllem4N  34764  pexmidlem1N  34775  lhp2atnle  34838  cdleme11dN  35068  cdleme20k  35126  cdleme21at  35135  cdleme21ct  35136  cdleme32e  35252  cdleme35f  35261  tendoex  35782  dochexmidlem1  36268  lcfrlem9  36358  mapd1o  36456  mapdindp3  36530  ismrc  36783  pellexlem1  36912  aomclem4  37146  dfac21  37155  lsmfgcl  37163  lmhmfgima  37173  dfacbasgrp  37198  hbtlem6  37219  fiuneneq  37295  mapsnd  38897  stoweidlem27  39581  stoweidlem29  39583  iccpartrn  40694  prmdvdsfmtnof1lem2  40826  mod42tp1mod8  40848  assintopass  41168
  Copyright terms: Public domain W3C validator