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

Theorem syl5ibcom 224
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 223 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 32 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  biimpcd  228  mob2  3220  rmob  3361  disjxun  4403  sotric  4784  sotrieq  4785  iss  5155  poirr2  5227  xp11  5275  nordeq  5445  nsuceq0  5506  suctr  5509  tz6.12c  5889  fnbrfvb  5910  foeqcnvco  6203  f1eqcocnv  6204  dfwe2  6613  mpt2sn  6892  tfrlem15  7115  tz7.44-2  7130  tz7.48-1  7165  tz7.49  7167  oawordexr  7262  oewordi  7297  oeeulem  7307  nna0r  7315  nnawordex  7343  nnaordex  7344  oaabs  7350  oaabs2  7351  ectocld  7435  ecoptocl  7458  mapsn  7518  eqeng  7608  difsnen  7659  fopwdom  7685  frfi  7821  elfiun  7949  ordiso  8036  ordtypelem7  8044  wemaplem2  8067  suc11reg  8129  inf3lem6  8143  noinfep  8170  cantnff  8184  cantnfp1lem2  8189  cantnfp1lem3  8190  cantnflem1  8199  cantnf  8203  r111  8251  rankc2  8347  tcrank  8360  cardnueq0  8403  fodomfi2  8496  alephinit  8531  dfac9  8571  dfac12k  8582  cdainf  8627  ackbij1  8673  ackbij2  8678  sornom  8712  fin23lem16  8770  fin23lem21  8774  isf32lem2  8789  fin1a2lem6  8840  itunitc  8856  zorn2lem4  8934  wunr1om  9149  tskr1om  9197  recmulnq  9394  ltexnq  9405  distrlem4pr  9456  1re  9647  0re  9648  0cnALT  9869  mulge0  10139  prodgt0  10457  peano2nn  10628  recnz  11018  zneo  11025  uzn0  11181  xlemul1a  11581  prunioo  11768  flidz  12053  ceilidz  12086  modid2  12131  om2uzrani  12173  uzrdgfni  12179  seqid  12265  seqz  12268  facdiv  12479  facwordi  12481  hashdom  12565  wrdnval  12704  wrdl1s1  12758  sqrmo  13327  fsumf1o  13801  isumltss  13918  supcvg  13926  dvdsnegb  14332  odd2np1lem  14376  odd2np1  14377  bitsuz  14460  bezoutlem4OLD  14518  bezoutlem4  14521  gcddiv  14529  gcdeq  14532  dvdssqim  14533  lcmgcdeq  14589  dvdsprm  14659  coprm  14669  coprmdvds2  14672  prmdvdsexp  14679  rpmul  14687  prmdiv  14745  opoe  14773  omoe  14774  opeo  14775  omeo  14776  pythagtriplem19  14795  pc2dvds  14840  pcadd  14846  prmpwdvds  14860  vdwlem11  14953  ramubcl  14988  0ram  14990  mreexexd  15566  posasymb  16210  pleval2  16223  pltval3  16225  plttr  16228  pospo  16231  letsr  16485  intopsn  16510  ismgmid  16519  imasmnd2  16585  isgrpid2  16714  isgrpinv  16728  imasgrp2  16813  orbsta  16979  symgfix2  17069  pmtrfrn  17111  pmtrrn2  17113  odmulg  17219  odmulgeq  17220  gexdvdsi  17246  gexnnod  17252  pgpssslw  17278  sylow2alem1  17281  fislw  17289  lsmss1b  17329  lsmss2b  17331  efgrelexlemb  17412  torsubg  17504  ablfacrplem  17710  pgpfac1lem2  17720  pgpfac1lem3  17722  imasring  17859  dvdsrcl2  17890  dvdsrtr  17892  dvdsrmul1  17893  irredn0  17943  lspsneq0  18247  lmhmima  18282  lspsolv  18378  opsrtoslem2  18720  mpfind  18771  mpfpf1  18951  pf1mpf  18952  xrsdsreclblem  19026  dvdsrzring  19064  prmirredlem  19076  znunit  19146  pjdm2  19286  obselocv  19303  lindfrn  19391  cpmadugsumlemF  19912  baspartn  19981  bastop  20009  iscld3  20092  isopn3  20094  iscldtop  20123  ordtrest2lem  20231  2ndcredom  20477  2ndc1stc  20478  2ndcrest  20481  2ndcdisj  20483  2ndcsep  20486  kgenidm  20574  dfac14  20645  tx2ndc  20678  kqreglem1  20768  rnelfm  20980  fmfnfmlem2  20982  fmfnfmlem4  20984  fmfnfm  20985  flimtopon  20997  fclstopon  21039  xrsmopn  21842  icccmplem2  21853  reconnlem1  21856  iccpnfcnv  21984  cphsqrtcl2  22176  ivthlem3  22416  ivthicc  22421  ovolctb  22455  ioombl  22530  itgabs  22804  itgsplitioo  22807  dvlip  22957  c1liplem1  22960  c1lip1  22961  dvgt0lem1  22966  dvivthlem2  22973  dvne0  22975  lhop1lem  22977  lhop1  22978  lhop2  22979  lhop  22980  dvcvx  22984  itgsubstlem  23012  mdegnn0cl  23032  ig1peu  23134  ig1peuOLD  23135  elply2  23162  plypf1  23178  dgreq0  23231  aannenlem3  23298  abelthlem2  23399  lognegb  23551  eflogeq  23563  efopn  23615  cxpge0  23640  cxplea  23653  cxple2  23654  cxpcn3lem  23699  cxpaddlelem  23703  cxpaddle  23704  cxpeq  23709  asinsinb  23835  acoscosb  23836  atantanb  23862  leibpilem1  23878  wilthlem2  24006  sqf11  24078  sqff1o  24121  ppiublem1  24142  lgsdir  24270  lgsne0  24273  lgsquadlem3  24296  2sqblem  24317  dchrisum0flblem1  24358  ostth3  24488  ostth  24489  colinearalg  24952  axcontlem5  25010  axcontlem9  25014  umgraf  25057  uslgraf1oedg  25098  nbgrassvwo  25177  usgrcyclnl1  25380  nvnencycllem  25383  clwwlknprop  25512  clwlkf1clwwlklem1  25586  usg2wlkonot  25623  usg2wotspth  25624  eupath2lem2  25718  eupath2lem3  25719  isgrp2d  25975  rngosn3  26166  htthlem  26582  pjpreeq  27063  h1dn0  27217  spansneleqi  27234  rnbra  27772  dfpjop  27847  elpjrn  27855  stm1i  27908  mdbr2  27961  mdsl2i  27987  sumdmdlem  28083  dmdbr6ati  28088  ordtrest2NEWlem  28740  xrge0iifcnv  28751  eulerpartlemb  29213  erdszelem8  29933  cvmlift3lem4  30057  cvmlift3lem5  30058  mrsub0  30166  mrsubccat  30168  mrsubcn  30169  msubrn  30179  msrid  30195  elmthm  30226  ghomgrpilem2  30316  dvdspw  30398  dfon2lem9  30449  poseq  30503  noseponlem  30567  nodenselem3  30584  nodenselem5  30586  nodenselem8  30589  nofulllem5  30607  btwnconn1lem11  30876  broutsideof2  30901  opnbnd  30993  tailfb  31045  fin2so  31944  poimirlem9  31961  poimirlem17  31969  poimirlem26  31978  poimirlem27  31979  poimirlem31  31983  itgabsnc  32023  ftc2nc  32038  sdclem2  32083  subspopn  32093  equivtotbnd  32122  igenval2  32311  isfldidl  32313  lshpinN  32567  lsatcv0eq  32625  lsatcv1  32626  cvrnbtwn3  32854  cvrnbtwn4  32857  cvrcmp  32861  atnlt  32891  cvlexchb1  32908  2llnne2N  32985  atcvr0eq  33003  lnnat  33004  cvrat4  33020  ps-1  33054  3at  33067  llncmp  33099  llnnlt  33100  llncvrlpln2  33134  llncvrlpln  33135  lplncmp  33139  lplnnlt  33142  lplncvrlvol2  33192  lplncvrlvol  33193  lvolcmp  33194  lvolnltN  33195  dalempnes  33228  dalemqnet  33229  dalem-cly  33248  dalem44  33293  lncmp  33360  cdlemblem  33370  llnexch2N  33447  osumcllem4N  33536  pexmidlem1N  33547  lhp2atnle  33610  cdleme11dN  33840  cdleme20k  33898  cdleme21at  33907  cdleme21ct  33908  cdleme32e  34024  cdleme35f  34033  tendoex  34554  dochexmidlem1  35040  lcfrlem9  35130  mapd1o  35228  mapdindp3  35302  ismrc  35555  pellexlem1  35685  aomclem4  35927  dfac21  35936  lsmfgcl  35944  lmhmfgima  35954  dfacbasgrp  35979  hbtlem6  36000  fiuneneq  36083  mapsnd  37486  stoweidlem27  37897  stoweidlem29  37899  stoweidlem29OLD  37900  iccpartrn  38754  gcdzeq  38803  uhgrn0  39168  upgrfn  39189  umgrfn  39199  uspgrf1oedg  39270  uvtxanbgrvtx  39475  vtxduhgr0nedg  39556  assintopass  39954
  Copyright terms: Public domain W3C validator