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

Theorem syl5ibcom 213
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 212 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  biimpcd  217  mob2  3115  rmob  3250  disjxun  4211  sotric  4530  sotrieq  4531  nordeq  4601  nsuceq0  4662  suctrALT  4665  dfwe2  4763  iss  5190  poirr2  5259  xp11  5305  tz6.12c  5751  fnbrfvb  5768  foeqcnvco  6028  f1eqcocnv  6029  tfrlem15  6654  tz7.44-2  6666  tz7.48-1  6701  tz7.49  6703  oawordexr  6800  oewordi  6835  oeeulem  6845  nna0r  6853  nnawordex  6881  nnaordex  6882  oaabs  6888  oaabs2  6889  ectocld  6972  ecoptocl  6995  mapsn  7056  eqeng  7142  difsnen  7191  fopwdom  7217  frfi  7353  elfiun  7436  ordiso  7486  ordtypelem7  7494  wemaplem2  7517  suc11reg  7575  inf3lem6  7589  noinfep  7615  cantnff  7630  cantnfp1lem2  7636  cantnfp1lem3  7637  cantnflem1  7646  cantnf  7650  r111  7702  rankc2  7798  tcrank  7809  cardnueq0  7852  fodomfi2  7942  alephinit  7977  dfac9  8017  dfac12k  8028  cdainf  8073  ackbij1  8119  ackbij2  8124  sornom  8158  fin23lem16  8216  fin23lem21  8220  isf32lem2  8235  fin1a2lem6  8286  itunitc  8302  zorn2lem4  8380  wunr1om  8595  tskr1om  8643  recmulnq  8842  ltexnq  8853  distrlem4pr  8904  1re  9091  0re  9092  0cnALT  9296  mulge0  9546  prodgt0  9856  peano2nn  10013  recnz  10346  zneo  10353  uzn0  10502  xlemul1a  10868  prunioo  11026  flidz  11219  modid2  11272  om2uzrani  11293  uzrdgfni  11299  seqid  11369  seqz  11372  facdiv  11579  facwordi  11581  hashdom  11654  sqrmo  12058  fsumf1o  12518  isumltss  12629  supcvg  12636  dvdsnegb  12868  odd2np1lem  12908  odd2np1  12909  bitsuz  12987  bezoutlem4  13042  gcddiv  13050  gcdeq  13053  dvdssqim  13054  dvdsprm  13100  coprm  13101  coprmdvds2  13104  prmdvdsexp  13115  rpmul  13124  prmdiv  13175  opoe  13186  omoe  13187  opeo  13188  omeo  13189  pythagtriplem19  13208  pc2dvds  13253  pcadd  13259  prmpwdvds  13273  vdwlem11  13360  ramubcl  13387  0ram  13389  mreexexd  13874  posasymb  14410  pleval2  14423  pltval3  14425  plttr  14428  pospo  14431  letsr  14673  ismgmid  14711  imasmnd2  14733  isgrpid2  14842  isgrpinv  14856  imasgrp2  14934  orbsta  15091  odmulg  15193  odmulgeq  15194  gexdvdsi  15218  gexnnod  15223  pgpssslw  15249  sylow2alem1  15252  fislw  15260  lsmss1b  15300  lsmss2b  15302  efgrelexlemb  15383  torsubg  15470  ablfacrplem  15624  pgpfac1lem2  15634  pgpfac1lem3  15636  imasrng  15726  dvdsrcl2  15756  dvdsrtr  15758  dvdsrmul1  15759  irredn0  15809  lspsneq0  16089  lmhmima  16124  lspsolv  16216  opsrtoslem2  16546  xrsdsreclblem  16745  dvdsrz  16768  prmirredlem  16774  znunit  16845  pjdm2  16939  obselocv  16956  baspartn  17020  bastop  17047  iscld3  17129  isopn3  17131  iscldtop  17160  ordtrest2lem  17268  2ndcredom  17514  2ndc1stc  17515  2ndcrest  17518  2ndcdisj  17520  2ndcsep  17523  kgenidm  17580  dfac14  17651  tx2ndc  17684  kqreglem1  17774  rnelfm  17986  fmfnfmlem2  17988  fmfnfmlem4  17990  fmfnfm  17991  flimtopon  18003  fclstopon  18045  xrsmopn  18844  icccmplem2  18855  reconnlem1  18858  iccpnfcnv  18970  cphsqrcl2  19150  ivthlem3  19351  ivthicc  19356  ovolctb  19387  ioombl  19460  itgabs  19727  itgsplitioo  19730  dvlip  19878  c1liplem1  19881  c1lip1  19882  dvgt0lem1  19887  dvivthlem2  19894  dvne0  19896  lhop1lem  19898  lhop1  19899  lhop2  19900  lhop  19901  dvcvx  19905  itgsubstlem  19933  mpfind  19966  mpfpf1  19972  pf1mpf  19973  mdegnn0cl  19995  ig1peu  20095  elply2  20116  plypf1  20132  dgreq0  20184  aannenlem3  20248  abelthlem2  20349  lognegb  20485  eflogeq  20497  efopn  20550  cxpge0  20575  cxplea  20588  cxple2  20589  cxpcn3lem  20632  cxpaddlelem  20636  cxpaddle  20637  cxpeq  20642  asinsinb  20738  acoscosb  20739  atantanb  20765  leibpilem1  20781  wilthlem2  20853  sqf11  20923  sqff1o  20966  ppiublem1  20987  lgsdir  21115  lgsne0  21118  lgsquadlem3  21141  2sqblem  21162  dchrisum0flblem1  21203  ostth3  21333  ostth  21334  umgraf  21354  usgrcyclnl1  21628  nvnencycllem  21631  eupath2lem2  21701  eupath2lem3  21702  isgrp2d  21824  rngosn3  22015  htthlem  22421  pjpreeq  22901  h1dn0  23055  spansneleqi  23072  rnbra  23611  dfpjop  23686  elpjrn  23694  stm1i  23747  mdbr2  23800  mdsl2i  23826  sumdmdlem  23922  dmdbr6ati  23927  xrge0iifcnv  24320  erdszelem8  24885  cvmlift3lem4  25010  cvmlift3lem5  25011  ghomgrpilem2  25098  dvdspw  25370  dfon2lem9  25419  poseq  25529  nodenselem3  25639  nodenselem5  25641  nodenselem8  25644  nofulllem5  25662  colinearalg  25850  axcontlem5  25908  axcontlem9  25912  btwnconn1lem11  26032  broutsideof2  26057  itgabsnc  26275  ftc2nc  26290  opnbnd  26329  tailfb  26407  sdclem2  26447  subspopn  26459  equivtotbnd  26488  igenval2  26677  isfldidl  26679  ismrc  26756  pellexlem1  26893  aomclem4  27133  dfac21  27142  lsmfgcl  27150  lmhmfgima  27160  dfacbasgrp  27251  lindfrn  27269  hbtlem6  27311  pmtrfrn  27378  fiuneneq  27491  xrltneNEW  27634  stoweidlem27  27753  stoweidlem29  27755  cshwsym  28274  usg2wlkonot  28351  usg2wotspth  28352  lshpinN  29788  lsatcv0eq  29846  lsatcv1  29847  cvrnbtwn3  30075  cvrnbtwn4  30078  cvrcmp  30082  atnlt  30112  cvlexchb1  30129  2llnne2N  30206  atcvr0eq  30224  lnnat  30225  cvrat4  30241  ps-1  30275  3at  30288  llncmp  30320  llnnlt  30321  llncvrlpln2  30355  llncvrlpln  30356  lplncmp  30360  lplnnlt  30363  lplncvrlvol2  30413  lplncvrlvol  30414  lvolcmp  30415  lvolnltN  30416  dalempnes  30449  dalemqnet  30450  dalem-cly  30469  dalem44  30514  lncmp  30581  cdlemblem  30591  llnexch2N  30668  osumcllem4N  30757  pexmidlem1N  30768  lhp2atnle  30831  cdleme11dN  31060  cdleme20k  31117  cdleme21at  31126  cdleme21ct  31127  cdleme32e  31243  cdleme35f  31252  tendoex  31773  dochexmidlem1  32259  lcfrlem9  32349  mapd1o  32447  mapdindp3  32521
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator