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

Theorem syl5ibcom 228
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 227 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 31 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189
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 190
This theorem is referenced by:  biimpcd  232  mob2  3206  rmob  3345  disjxun  4393  sotric  4786  sotrieq  4787  iss  5158  poirr2  5230  xp11  5278  nordeq  5449  nsuceq0  5510  suctr  5513  tz6.12c  5898  fnbrfvb  5919  foeqcnvco  6216  f1eqcocnv  6217  dfwe2  6627  mpt2sn  6906  tfrlem15  7128  tz7.44-2  7143  tz7.48-1  7178  tz7.49  7180  oawordexr  7275  oewordi  7310  oeeulem  7320  nna0r  7328  nnawordex  7356  nnaordex  7357  oaabs  7363  oaabs2  7364  ectocld  7448  ecoptocl  7471  mapsn  7531  eqeng  7621  difsnen  7672  fopwdom  7698  frfi  7834  elfiun  7962  ordiso  8049  ordtypelem7  8057  wemaplem2  8080  suc11reg  8142  inf3lem6  8156  noinfep  8183  cantnff  8197  cantnfp1lem2  8202  cantnfp1lem3  8203  cantnflem1  8212  cantnf  8216  r111  8264  rankc2  8360  tcrank  8373  cardnueq0  8416  fodomfi2  8509  alephinit  8544  dfac9  8584  dfac12k  8595  cdainf  8640  ackbij1  8686  ackbij2  8691  sornom  8725  fin23lem16  8783  fin23lem21  8787  isf32lem2  8802  fin1a2lem6  8853  itunitc  8869  zorn2lem4  8947  wunr1om  9162  tskr1om  9210  recmulnq  9407  ltexnq  9418  distrlem4pr  9469  1re  9660  0re  9661  0cnALT  9884  mulge0  10153  prodgt0  10472  peano2nn  10643  recnz  11034  zneo  11041  uzn0  11198  xlemul1a  11599  prunioo  11787  flidz  12079  ceilidz  12112  modid2  12157  om2uzrani  12204  uzrdgfni  12210  seqid  12296  seqz  12299  facdiv  12510  facwordi  12512  hashdom  12596  wrdnval  12748  wrdl1s1  12805  sqrmo  13392  fsumf1o  13866  isumltss  13983  supcvg  13991  dvdsnegb  14397  odd2np1lem  14442  odd2np1  14443  bitsuz  14527  bezoutlem4OLD  14585  bezoutlem4  14588  gcddiv  14596  gcdeq  14599  dvdssqim  14600  lcmgcdeq  14656  dvdsprm  14726  coprm  14736  coprmdvds2  14739  prmdvdsexp  14746  rpmul  14754  prmdiv  14812  opoe  14840  omoe  14841  opeo  14842  omeo  14843  pythagtriplem19  14862  pc2dvds  14907  pcadd  14913  prmpwdvds  14927  vdwlem11  15020  ramubcl  15055  0ram  15057  mreexexd  15632  posasymb  16276  pleval2  16289  pltval3  16291  plttr  16294  pospo  16297  letsr  16551  intopsn  16576  ismgmid  16585  imasmnd2  16651  isgrpid2  16780  isgrpinv  16794  imasgrp2  16879  orbsta  17045  symgfix2  17135  pmtrfrn  17177  pmtrrn2  17179  odmulg  17285  odmulgeq  17286  gexdvdsi  17312  gexnnod  17318  pgpssslw  17344  sylow2alem1  17347  fislw  17355  lsmss1b  17395  lsmss2b  17397  efgrelexlemb  17478  torsubg  17570  ablfacrplem  17776  pgpfac1lem2  17786  pgpfac1lem3  17788  imasring  17925  dvdsrcl2  17956  dvdsrtr  17958  dvdsrmul1  17959  irredn0  18009  lspsneq0  18313  lmhmima  18348  lspsolv  18444  opsrtoslem2  18785  mpfind  18836  mpfpf1  19016  pf1mpf  19017  xrsdsreclblem  19091  dvdsrzring  19129  prmirredlem  19141  znunit  19211  pjdm2  19351  obselocv  19368  lindfrn  19456  cpmadugsumlemF  19977  baspartn  20046  bastop  20074  iscld3  20157  isopn3  20159  iscldtop  20188  ordtrest2lem  20296  2ndcredom  20542  2ndc1stc  20543  2ndcrest  20546  2ndcdisj  20548  2ndcsep  20551  kgenidm  20639  dfac14  20710  tx2ndc  20743  kqreglem1  20833  rnelfm  21046  fmfnfmlem2  21048  fmfnfmlem4  21050  fmfnfm  21051  flimtopon  21063  fclstopon  21105  xrsmopn  21908  icccmplem2  21919  reconnlem1  21922  iccpnfcnv  22050  cphsqrtcl2  22242  ivthlem3  22482  ivthicc  22487  ovolctb  22521  ioombl  22597  itgabs  22871  itgsplitioo  22874  dvlip  23024  c1liplem1  23027  c1lip1  23028  dvgt0lem1  23033  dvivthlem2  23040  dvne0  23042  lhop1lem  23044  lhop1  23045  lhop2  23046  lhop  23047  dvcvx  23051  itgsubstlem  23079  mdegnn0cl  23099  ig1peu  23201  ig1peuOLD  23202  elply2  23229  plypf1  23245  dgreq0  23298  aannenlem3  23365  abelthlem2  23466  lognegb  23618  eflogeq  23630  efopn  23682  cxpge0  23707  cxplea  23720  cxple2  23721  cxpcn3lem  23766  cxpaddlelem  23770  cxpaddle  23771  cxpeq  23776  asinsinb  23902  acoscosb  23903  atantanb  23929  leibpilem1  23945  wilthlem2  24073  sqf11  24145  sqff1o  24188  ppiublem1  24209  lgsdir  24337  lgsne0  24340  lgsquadlem3  24363  2sqblem  24384  dchrisum0flblem1  24425  ostth3  24555  ostth  24556  colinearalg  25019  axcontlem5  25077  axcontlem9  25081  umgraf  25124  uslgraf1oedg  25165  nbgrassvwo  25244  usgrcyclnl1  25447  nvnencycllem  25450  clwwlknprop  25579  clwlkf1clwwlklem1  25653  usg2wlkonot  25690  usg2wotspth  25691  eupath2lem2  25785  eupath2lem3  25786  isgrp2d  26044  rngosn3  26235  htthlem  26651  pjpreeq  27132  h1dn0  27286  spansneleqi  27303  rnbra  27841  dfpjop  27916  elpjrn  27924  stm1i  27977  mdbr2  28030  mdsl2i  28056  sumdmdlem  28152  dmdbr6ati  28157  ordtrest2NEWlem  28802  xrge0iifcnv  28813  eulerpartlemb  29274  erdszelem8  29993  cvmlift3lem4  30117  cvmlift3lem5  30118  mrsub0  30226  mrsubccat  30228  mrsubcn  30229  msubrn  30239  msrid  30255  elmthm  30286  ghomgrpilem2  30376  dvdspw  30457  dfon2lem9  30508  poseq  30562  noseponlem  30626  nodenselem3  30643  nodenselem5  30645  nodenselem8  30648  nofulllem5  30666  btwnconn1lem11  30935  broutsideof2  30960  opnbnd  31052  tailfb  31104  fin2so  31996  poimirlem9  32013  poimirlem17  32021  poimirlem26  32030  poimirlem27  32031  poimirlem31  32035  itgabsnc  32075  ftc2nc  32090  sdclem2  32135  subspopn  32145  equivtotbnd  32174  igenval2  32363  isfldidl  32365  lshpinN  32626  lsatcv0eq  32684  lsatcv1  32685  cvrnbtwn3  32913  cvrnbtwn4  32916  cvrcmp  32920  atnlt  32950  cvlexchb1  32967  2llnne2N  33044  atcvr0eq  33062  lnnat  33063  cvrat4  33079  ps-1  33113  3at  33126  llncmp  33158  llnnlt  33159  llncvrlpln2  33193  llncvrlpln  33194  lplncmp  33198  lplnnlt  33201  lplncvrlvol2  33251  lplncvrlvol  33252  lvolcmp  33253  lvolnltN  33254  dalempnes  33287  dalemqnet  33288  dalem-cly  33307  dalem44  33352  lncmp  33419  cdlemblem  33429  llnexch2N  33506  osumcllem4N  33595  pexmidlem1N  33606  lhp2atnle  33669  cdleme11dN  33899  cdleme20k  33957  cdleme21at  33966  cdleme21ct  33967  cdleme32e  34083  cdleme35f  34092  tendoex  34613  dochexmidlem1  35099  lcfrlem9  35189  mapd1o  35287  mapdindp3  35361  ismrc  35614  pellexlem1  35744  aomclem4  35986  dfac21  35995  lsmfgcl  36003  lmhmfgima  36013  dfacbasgrp  36038  hbtlem6  36059  fiuneneq  36142  mapsnd  37547  stoweidlem27  37999  stoweidlem29  38001  stoweidlem29OLD  38002  iccpartrn  38889  gcdzeq  38938  uhgrn0  39311  upgrfn  39333  umgrfn  39344  uspgrf1oedg  39421  uvtxanbgrvtx  39629  vtxduhgr0nedg  39715  pthdivtx  39922  eupth2lem2  40131  eupth2lem3lem6  40145  assintopass  40358
  Copyright terms: Public domain W3C validator