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

Theorem syl5ibcom 211
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 210 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 27 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  biimpcd  215  mob2  2945  rmob  3079  disjxun  4021  sotric  4340  sotrieq  4341  nordeq  4411  nsuceq0  4472  suctr  4475  dfwe2  4573  iss  4998  poirr2  5067  xp11  5111  tz6.12c  5547  fnbrfvb  5563  foeqcnvco  5804  f1eqcocnv  5805  tfrlem15  6408  tz7.44-2  6420  tz7.48-1  6455  tz7.49  6457  oawordexr  6554  oewordi  6589  oeeulem  6599  nna0r  6607  nnawordex  6635  nnaordex  6636  oaabs  6642  oaabs2  6643  ectocld  6726  ecoptocl  6748  mapsn  6809  eqeng  6895  difsnen  6944  fopwdom  6970  frfi  7102  elfiun  7183  ordiso  7231  ordtypelem7  7239  wemaplem2  7262  suc11reg  7320  inf3lem6  7334  noinfep  7360  cantnff  7375  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1  7391  cantnf  7395  r111  7447  rankc2  7543  tcrank  7554  cardnueq0  7597  fodomfi2  7687  alephinit  7722  dfac9  7762  dfac12k  7773  cdainf  7818  ackbij1  7864  ackbij2  7869  sornom  7903  fin23lem16  7961  fin23lem21  7965  isf32lem2  7980  fin1a2lem6  8031  itunitc  8047  zorn2lem4  8126  wunr1om  8341  tskr1om  8389  recmulnq  8588  ltexnq  8599  distrlem4pr  8650  1re  8837  0re  8838  0cnALT  9041  mulge0  9291  prodgt0  9601  peano2nn  9758  recnz  10087  zneo  10094  uzn0  10243  xlemul1a  10608  prunioo  10764  flidz  10941  modid2  10994  om2uzrani  11015  uzrdgfni  11021  seqid  11091  seqz  11094  facdiv  11300  facwordi  11302  hashdom  11361  sqrmo  11737  fsumf1o  12196  isumltss  12307  supcvg  12314  dvdsnegb  12546  odd2np1lem  12586  odd2np1  12587  bitsuz  12665  bezoutlem4  12720  gcddiv  12728  gcdeq  12731  dvdssqim  12732  dvdsprm  12778  coprm  12779  coprmdvds2  12782  prmdvdsexp  12793  rpmul  12802  prmdiv  12853  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pythagtriplem19  12886  pc2dvds  12931  pcadd  12937  prmpwdvds  12951  vdwlem11  13038  ramubcl  13065  0ram  13067  mreexexd  13550  posasymb  14086  pleval2  14099  pltval3  14101  plttr  14104  pospo  14107  letsr  14349  ismgmid  14387  imasmnd2  14409  isgrpid2  14518  isgrpinv  14532  imasgrp2  14610  orbsta  14767  odmulg  14869  odmulgeq  14870  gexdvdsi  14894  gexnnod  14899  pgpssslw  14925  sylow2alem1  14928  fislw  14936  lsmss1b  14976  lsmss2b  14978  efgrelexlemb  15059  torsubg  15146  ablfacrplem  15300  pgpfac1lem2  15310  pgpfac1lem3  15312  imasrng  15402  dvdsrcl2  15432  dvdsrtr  15434  dvdsrmul1  15435  irredn0  15485  lspsneq0  15769  lmhmima  15804  lspsolv  15896  opsrtoslem2  16226  xrsdsreclblem  16417  dvdsrz  16440  prmirredlem  16446  znunit  16517  pjdm2  16611  obselocv  16628  baspartn  16692  bastop  16719  iscld3  16801  isopn3  16803  iscldtop  16832  ordtrest2lem  16933  2ndcredom  17176  2ndc1stc  17177  2ndcrest  17180  2ndcdisj  17182  2ndcsep  17185  kgenidm  17242  dfac14  17312  tx2ndc  17345  kqreglem1  17432  rnelfm  17648  fmfnfmlem2  17650  fmfnfmlem4  17652  fmfnfm  17653  flimtopon  17665  fclstopon  17707  xrsmopn  18318  icccmplem2  18328  reconnlem1  18331  iccpnfcnv  18442  cphsqrcl2  18622  ivthlem3  18813  ivthicc  18818  ovolctb  18849  ioombl  18922  itgabs  19189  itgsplitioo  19192  dvlip  19340  c1liplem1  19343  c1lip1  19344  dvgt0lem1  19349  dvivthlem2  19356  dvne0  19358  lhop1lem  19360  lhop1  19361  lhop2  19362  lhop  19363  dvcvx  19367  itgsubstlem  19395  mpfind  19428  mpfpf1  19434  pf1mpf  19435  mdegnn0cl  19457  ig1peu  19557  elply2  19578  plypf1  19594  dgreq0  19646  aannenlem3  19710  abelthlem2  19808  lognegb  19943  eflogeq  19955  efopn  20005  cxpge0  20030  cxplea  20043  cxple2  20044  cxpcn3lem  20087  cxpaddlelem  20091  cxpaddle  20092  cxpeq  20097  asinsinb  20193  acoscosb  20194  atantanb  20220  leibpilem1  20236  wilthlem2  20307  sqf11  20377  sqff1o  20420  ppiublem1  20441  lgsdir  20569  lgsne0  20572  lgsquadlem3  20595  2sqblem  20616  dchrisum0flblem1  20657  ostth3  20787  ostth  20788  isgrp2d  20902  rngosn3  21093  htthlem  21497  pjpreeq  21977  h1dn0  22131  spansneleqi  22148  rnbra  22687  dfpjop  22762  elpjrn  22770  stm1i  22823  mdbr2  22876  mdsl2i  22902  sumdmdlem  22998  dmdbr6ati  23003  xrge0iifcnv  23315  erdszelem8  23729  cvmlift3lem4  23853  cvmlift3lem5  23854  umgraf  23870  eupath2lem2  23902  eupath2lem3  23903  ghomgrpilem2  23993  dvdspw  24103  dfon2lem9  24147  poseq  24253  nodenselem3  24337  nodenselem5  24339  nodenselem8  24342  nofulllem5  24360  colinearalg  24538  axcontlem5  24596  axcontlem9  24600  btwnconn1lem11  24720  broutsideof2  24745  twsymr  25078  apnei  25520  fil2ss  25557  fnctartar  25907  fnctartar2  25908  opnbnd  26243  tailfb  26326  sdclem2  26452  subspopn  26466  equivtotbnd  26502  igenval2  26691  isfldidl  26693  ismrc  26776  pellexlem1  26914  aomclem4  27154  dfac21  27164  lsmfgcl  27172  lmhmfgima  27182  dfacbasgrp  27273  lindfrn  27291  hbtlem6  27333  pmtrfrn  27400  fiuneneq  27513  xrltneNEW  27657  stoweidlem27  27776  stoweidlem29  27778  lshpinN  29179  lsatcv0eq  29237  lsatcv1  29238  cvrnbtwn3  29466  cvrnbtwn4  29469  cvrcmp  29473  atnlt  29503  cvlexchb1  29520  2llnne2N  29597  atcvr0eq  29615  lnnat  29616  cvrat4  29632  ps-1  29666  3at  29679  llncmp  29711  llnnlt  29712  llncvrlpln2  29746  llncvrlpln  29747  lplncmp  29751  lplnnlt  29754  lplncvrlvol2  29804  lplncvrlvol  29805  lvolcmp  29806  lvolnltN  29807  dalempnes  29840  dalemqnet  29841  dalem-cly  29860  dalem44  29905  lncmp  29972  cdlemblem  29982  llnexch2N  30059  osumcllem4N  30148  pexmidlem1N  30159  lhp2atnle  30222  cdleme11dN  30451  cdleme20k  30508  cdleme21at  30517  cdleme21ct  30518  cdleme32e  30634  cdleme35f  30643  tendoex  31164  dochexmidlem1  31650  lcfrlem9  31740  mapd1o  31838  mapdindp3  31912
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 177
  Copyright terms: Public domain W3C validator