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  3265  rmob  3416  disjxun  4435  sotric  4816  sotrieq  4817  nordeq  4887  nsuceq0  4948  suctr  4951  iss  5311  poirr2  5381  xp11  5432  tz6.12c  5875  fnbrfvb  5898  foeqcnvco  6188  f1eqcocnv  6189  dfwe2  6602  mpt2sn  6876  tfrlem15  7063  tz7.44-2  7075  tz7.48-1  7110  tz7.49  7112  oawordexr  7207  oewordi  7242  oeeulem  7252  nna0r  7260  nnawordex  7288  nnaordex  7289  oaabs  7295  oaabs2  7296  ectocld  7380  ecoptocl  7403  mapsn  7462  eqeng  7551  difsnen  7601  fopwdom  7627  frfi  7767  elfiun  7892  ordiso  7944  ordtypelem7  7952  wemaplem2  7975  suc11reg  8039  inf3lem6  8053  noinfep  8079  cantnff  8096  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnflem1  8111  cantnf  8115  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1OLD  8134  cantnfOLD  8137  r111  8196  rankc2  8292  tcrank  8305  cardnueq0  8348  fodomfi2  8444  alephinit  8479  dfac9  8519  dfac12k  8530  cdainf  8575  ackbij1  8621  ackbij2  8626  sornom  8660  fin23lem16  8718  fin23lem21  8722  isf32lem2  8737  fin1a2lem6  8788  itunitc  8804  zorn2lem4  8882  wunr1om  9100  tskr1om  9148  recmulnq  9345  ltexnq  9356  distrlem4pr  9407  1re  9598  0re  9599  0cnALT  9814  mulge0  10077  prodgt0  10394  peano2nn  10555  recnz  10945  zneo  10952  uzn0  11107  xlemul1a  11491  prunioo  11660  flidz  11929  ceilidz  11961  modid2  12005  om2uzrani  12045  uzrdgfni  12051  seqid  12134  seqz  12137  facdiv  12347  facwordi  12349  hashdom  12429  wrdnval  12553  wrdl1s1  12604  sqrmo  13067  fsumf1o  13527  isumltss  13642  supcvg  13649  dvdsnegb  13983  odd2np1lem  14027  odd2np1  14028  bitsuz  14106  bezoutlem4  14161  gcddiv  14169  gcdeq  14172  dvdssqim  14173  dvdsprm  14222  coprm  14223  coprmdvds2  14226  prmdvdsexp  14237  rpmul  14246  prmdiv  14297  opoe  14317  omoe  14318  opeo  14319  omeo  14320  pythagtriplem19  14339  pc2dvds  14384  pcadd  14390  prmpwdvds  14404  vdwlem11  14491  ramubcl  14518  0ram  14520  mreexexd  15027  posasymb  15561  pleval2  15574  pltval3  15576  plttr  15579  pospo  15582  letsr  15836  intopsn  15861  ismgmid  15870  imasmnd2  15936  isgrpid2  16065  isgrpinv  16079  imasgrp2  16164  orbsta  16330  symgfix2  16420  pmtrfrn  16462  pmtrrn2  16464  odmulg  16557  odmulgeq  16558  gexdvdsi  16582  gexnnod  16587  pgpssslw  16613  sylow2alem1  16616  fislw  16624  lsmss1b  16664  lsmss2b  16666  efgrelexlemb  16747  torsubg  16839  ablfacrplem  17095  pgpfac1lem2  17105  pgpfac1lem3  17107  imasring  17247  dvdsrcl2  17278  dvdsrtr  17280  dvdsrmul1  17281  irredn0  17331  lspsneq0  17637  lmhmima  17672  lspsolv  17768  opsrtoslem2  18128  mpfind  18184  mpfpf1  18366  pf1mpf  18367  xrsdsreclblem  18443  dvdsrzring  18485  dvdsrz  18486  prmirredlem  18501  prmirredlemOLD  18504  znunit  18580  pjdm2  18720  obselocv  18737  lindfrn  18834  cpmadugsumlemF  19355  baspartn  19433  bastop  19461  iscld3  19543  isopn3  19545  iscldtop  19574  ordtrest2lem  19682  2ndcredom  19929  2ndc1stc  19930  2ndcrest  19933  2ndcdisj  19935  2ndcsep  19938  kgenidm  20026  dfac14  20097  tx2ndc  20130  kqreglem1  20220  rnelfm  20432  fmfnfmlem2  20434  fmfnfmlem4  20436  fmfnfm  20437  flimtopon  20449  fclstopon  20491  xrsmopn  21295  icccmplem2  21306  reconnlem1  21309  iccpnfcnv  21422  cphsqrtcl2  21611  ivthlem3  21843  ivthicc  21848  ovolctb  21879  ioombl  21953  itgabs  22219  itgsplitioo  22222  dvlip  22372  c1liplem1  22375  c1lip1  22376  dvgt0lem1  22381  dvivthlem2  22388  dvne0  22390  lhop1lem  22392  lhop1  22393  lhop2  22394  lhop  22395  dvcvx  22399  itgsubstlem  22427  mdegnn0cl  22449  ig1peu  22550  elply2  22571  plypf1  22587  dgreq0  22640  aannenlem3  22704  abelthlem2  22805  lognegb  22952  eflogeq  22964  efopn  23017  cxpge0  23042  cxplea  23055  cxple2  23056  cxpcn3lem  23099  cxpaddlelem  23103  cxpaddle  23104  cxpeq  23109  asinsinb  23206  acoscosb  23207  atantanb  23233  leibpilem1  23249  wilthlem2  23321  sqf11  23391  sqff1o  23434  ppiublem1  23455  lgsdir  23583  lgsne0  23586  lgsquadlem3  23609  2sqblem  23630  dchrisum0flblem1  23671  ostth3  23801  ostth  23802  colinearalg  24191  axcontlem5  24249  axcontlem9  24253  umgraf  24296  uslgraf1oedg  24337  nbgrassvwo  24415  usgrcyclnl1  24618  nvnencycllem  24621  clwwlknprop  24750  clwlkf1clwwlklem1  24824  usg2wlkonot  24861  usg2wotspth  24862  eupath2lem2  24956  eupath2lem3  24957  isgrp2d  25215  rngosn3  25406  htthlem  25812  pjpreeq  26294  h1dn0  26448  spansneleqi  26465  rnbra  27004  dfpjop  27079  elpjrn  27087  stm1i  27140  mdbr2  27193  mdsl2i  27219  sumdmdlem  27315  dmdbr6ati  27320  ordtrest2NEWlem  27882  xrge0iifcnv  27893  eulerpartlemb  28285  erdszelem8  28620  cvmlift3lem4  28745  cvmlift3lem5  28746  mrsub0  28854  mrsubccat  28856  mrsubcn  28857  msubrn  28867  msrid  28883  elmthm  28914  ghomgrpilem2  29004  dvdspw  29151  dfon2lem9  29199  poseq  29309  nodenselem3  29419  nodenselem5  29421  nodenselem8  29424  nofulllem5  29442  btwnconn1lem11  29723  broutsideof2  29748  fin2so  30016  itgabsnc  30060  ftc2nc  30075  opnbnd  30119  tailfb  30171  sdclem2  30211  subspopn  30221  equivtotbnd  30250  igenval2  30439  isfldidl  30441  ismrc  30609  pellexlem1  30741  aomclem4  30979  dfac21  30988  lsmfgcl  30996  lmhmfgima  31006  dfacbasgrp  31033  hbtlem6  31054  fiuneneq  31130  lcmgcdeq  31192  stoweidlem27  31763  stoweidlem29  31765  assintopass  32491  lshpinN  34589  lsatcv0eq  34647  lsatcv1  34648  cvrnbtwn3  34876  cvrnbtwn4  34879  cvrcmp  34883  atnlt  34913  cvlexchb1  34930  2llnne2N  35007  atcvr0eq  35025  lnnat  35026  cvrat4  35042  ps-1  35076  3at  35089  llncmp  35121  llnnlt  35122  llncvrlpln2  35156  llncvrlpln  35157  lplncmp  35161  lplnnlt  35164  lplncvrlvol2  35214  lplncvrlvol  35215  lvolcmp  35216  lvolnltN  35217  dalempnes  35250  dalemqnet  35251  dalem-cly  35270  dalem44  35315  lncmp  35382  cdlemblem  35392  llnexch2N  35469  osumcllem4N  35558  pexmidlem1N  35569  lhp2atnle  35632  cdleme11dN  35862  cdleme20k  35920  cdleme21at  35929  cdleme21ct  35930  cdleme32e  36046  cdleme35f  36055  tendoex  36576  dochexmidlem1  37062  lcfrlem9  37152  mapd1o  37250  mapdindp3  37324
  Copyright terms: Public domain W3C validator