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

Theorem syl5ibcom 220
Description: A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)
Hypotheses
Ref Expression
syl5ib.1  |-  ( ph  ->  ps )
syl5ib.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ibcom  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem syl5ibcom
StepHypRef Expression
1 syl5ib.1 . . 3  |-  ( ph  ->  ps )
2 syl5ib.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
31, 2syl5ib 219 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 31 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  biimpcd  224  mob2  3204  rmob  3344  disjxun  4365  sotric  4740  sotrieq  4741  nordeq  4811  nsuceq0  4872  suctr  4875  iss  5233  poirr2  5304  xp11  5352  tz6.12c  5793  fnbrfvb  5814  foeqcnvco  6104  f1eqcocnv  6105  dfwe2  6516  mpt2sn  6790  tfrlem15  6979  tz7.44-2  6991  tz7.48-1  7026  tz7.49  7028  oawordexr  7123  oewordi  7158  oeeulem  7168  nna0r  7176  nnawordex  7204  nnaordex  7205  oaabs  7211  oaabs2  7212  ectocld  7296  ecoptocl  7319  mapsn  7379  eqeng  7468  difsnen  7518  fopwdom  7544  frfi  7680  elfiun  7805  ordiso  7856  ordtypelem7  7864  wemaplem2  7887  suc11reg  7950  inf3lem6  7964  noinfep  7990  cantnff  8006  cantnfp1lem2  8011  cantnfp1lem3  8012  cantnflem1  8021  cantnf  8025  cantnfp1lem2OLD  8037  cantnfp1lem3OLD  8038  cantnflem1OLD  8044  cantnfOLD  8047  r111  8106  rankc2  8202  tcrank  8215  cardnueq0  8258  fodomfi2  8354  alephinit  8389  dfac9  8429  dfac12k  8440  cdainf  8485  ackbij1  8531  ackbij2  8536  sornom  8570  fin23lem16  8628  fin23lem21  8632  isf32lem2  8647  fin1a2lem6  8698  itunitc  8714  zorn2lem4  8792  wunr1om  9008  tskr1om  9056  recmulnq  9253  ltexnq  9264  distrlem4pr  9315  1re  9506  0re  9507  0cnALT  9722  mulge0  9988  prodgt0  10304  peano2nn  10464  recnz  10855  zneo  10862  uzn0  11016  xlemul1a  11401  prunioo  11570  flidz  11846  ceilidz  11879  modid2  11924  om2uzrani  11966  uzrdgfni  11972  seqid  12055  seqz  12058  facdiv  12267  facwordi  12269  hashdom  12350  wrdnval  12479  wrdl1s1  12531  sqrmo  13087  fsumf1o  13547  isumltss  13662  supcvg  13669  dvdsnegb  14003  odd2np1lem  14047  odd2np1  14048  bitsuz  14126  bezoutlem4  14181  gcddiv  14189  gcdeq  14192  dvdssqim  14193  dvdsprm  14242  coprm  14243  coprmdvds2  14246  prmdvdsexp  14257  rpmul  14266  prmdiv  14317  opoe  14337  omoe  14338  opeo  14339  omeo  14340  pythagtriplem19  14359  pc2dvds  14404  pcadd  14410  prmpwdvds  14424  vdwlem11  14511  ramubcl  14538  0ram  14540  mreexexd  15055  posasymb  15699  pleval2  15712  pltval3  15714  plttr  15717  pospo  15720  letsr  15974  intopsn  15999  ismgmid  16008  imasmnd2  16074  isgrpid2  16203  isgrpinv  16217  imasgrp2  16302  orbsta  16468  symgfix2  16558  pmtrfrn  16600  pmtrrn2  16602  odmulg  16695  odmulgeq  16696  gexdvdsi  16720  gexnnod  16725  pgpssslw  16751  sylow2alem1  16754  fislw  16762  lsmss1b  16802  lsmss2b  16804  efgrelexlemb  16885  torsubg  16977  ablfacrplem  17229  pgpfac1lem2  17239  pgpfac1lem3  17241  imasring  17381  dvdsrcl2  17412  dvdsrtr  17414  dvdsrmul1  17415  irredn0  17465  lspsneq0  17771  lmhmima  17806  lspsolv  17902  opsrtoslem2  18262  mpfind  18318  mpfpf1  18500  pf1mpf  18501  xrsdsreclblem  18577  dvdsrzring  18614  prmirredlem  18623  znunit  18693  pjdm2  18833  obselocv  18850  lindfrn  18941  cpmadugsumlemF  19462  baspartn  19540  bastop  19568  iscld3  19651  isopn3  19653  iscldtop  19682  ordtrest2lem  19790  2ndcredom  20036  2ndc1stc  20037  2ndcrest  20040  2ndcdisj  20042  2ndcsep  20045  kgenidm  20133  dfac14  20204  tx2ndc  20237  kqreglem1  20327  rnelfm  20539  fmfnfmlem2  20541  fmfnfmlem4  20543  fmfnfm  20544  flimtopon  20556  fclstopon  20598  xrsmopn  21402  icccmplem2  21413  reconnlem1  21416  iccpnfcnv  21529  cphsqrtcl2  21718  ivthlem3  21950  ivthicc  21955  ovolctb  21986  ioombl  22060  itgabs  22326  itgsplitioo  22329  dvlip  22479  c1liplem1  22482  c1lip1  22483  dvgt0lem1  22488  dvivthlem2  22495  dvne0  22497  lhop1lem  22499  lhop1  22500  lhop2  22501  lhop  22502  dvcvx  22506  itgsubstlem  22534  mdegnn0cl  22556  ig1peu  22657  elply2  22678  plypf1  22694  dgreq0  22747  aannenlem3  22811  abelthlem2  22912  lognegb  23062  eflogeq  23074  efopn  23126  cxpge0  23151  cxplea  23164  cxple2  23165  cxpcn3lem  23208  cxpaddlelem  23212  cxpaddle  23213  cxpeq  23218  asinsinb  23344  acoscosb  23345  atantanb  23371  leibpilem1  23387  wilthlem2  23460  sqf11  23530  sqff1o  23573  ppiublem1  23594  lgsdir  23722  lgsne0  23725  lgsquadlem3  23748  2sqblem  23769  dchrisum0flblem1  23810  ostth3  23940  ostth  23941  colinearalg  24334  axcontlem5  24392  axcontlem9  24396  umgraf  24439  uslgraf1oedg  24480  nbgrassvwo  24558  usgrcyclnl1  24761  nvnencycllem  24764  clwwlknprop  24893  clwlkf1clwwlklem1  24967  usg2wlkonot  25004  usg2wotspth  25005  eupath2lem2  25099  eupath2lem3  25100  isgrp2d  25354  rngosn3  25545  htthlem  25951  pjpreeq  26433  h1dn0  26587  spansneleqi  26604  rnbra  27142  dfpjop  27217  elpjrn  27225  stm1i  27278  mdbr2  27331  mdsl2i  27357  sumdmdlem  27453  dmdbr6ati  27458  ordtrest2NEWlem  28058  xrge0iifcnv  28069  eulerpartlemb  28490  erdszelem8  28831  cvmlift3lem4  28956  cvmlift3lem5  28957  mrsub0  29065  mrsubccat  29067  mrsubcn  29068  msubrn  29078  msrid  29094  elmthm  29125  ghomgrpilem2  29215  dvdspw  29341  dfon2lem9  29388  poseq  29498  nodenselem3  29608  nodenselem5  29610  nodenselem8  29613  nofulllem5  29631  btwnconn1lem11  29900  broutsideof2  29925  fin2so  30205  itgabsnc  30250  ftc2nc  30265  opnbnd  30309  tailfb  30361  sdclem2  30401  subspopn  30411  equivtotbnd  30440  igenval2  30629  isfldidl  30631  ismrc  30799  pellexlem1  30930  aomclem4  31169  dfac21  31178  lsmfgcl  31186  lmhmfgima  31196  dfacbasgrp  31225  hbtlem6  31246  fiuneneq  31322  lcmgcdeq  31384  stoweidlem27  31975  stoweidlem29  31977  gcdzeq  32506  assintopass  32856  lshpinN  35127  lsatcv0eq  35185  lsatcv1  35186  cvrnbtwn3  35414  cvrnbtwn4  35417  cvrcmp  35421  atnlt  35451  cvlexchb1  35468  2llnne2N  35545  atcvr0eq  35563  lnnat  35564  cvrat4  35580  ps-1  35614  3at  35627  llncmp  35659  llnnlt  35660  llncvrlpln2  35694  llncvrlpln  35695  lplncmp  35699  lplnnlt  35702  lplncvrlvol2  35752  lplncvrlvol  35753  lvolcmp  35754  lvolnltN  35755  dalempnes  35788  dalemqnet  35789  dalem-cly  35808  dalem44  35853  lncmp  35920  cdlemblem  35930  llnexch2N  36007  osumcllem4N  36096  pexmidlem1N  36107  lhp2atnle  36170  cdleme11dN  36400  cdleme20k  36458  cdleme21at  36467  cdleme21ct  36468  cdleme32e  36584  cdleme35f  36593  tendoex  37114  dochexmidlem1  37600  lcfrlem9  37690  mapd1o  37788  mapdindp3  37862
  Copyright terms: Public domain W3C validator