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  2958  rmob  3092  disjxun  4037  sotric  4356  sotrieq  4357  nordeq  4427  nsuceq0  4488  suctr  4491  dfwe2  4589  iss  5014  poirr2  5083  xp11  5127  tz6.12c  5563  fnbrfvb  5579  foeqcnvco  5820  f1eqcocnv  5821  tfrlem15  6424  tz7.44-2  6436  tz7.48-1  6471  tz7.49  6473  oawordexr  6570  oewordi  6605  oeeulem  6615  nna0r  6623  nnawordex  6651  nnaordex  6652  oaabs  6658  oaabs2  6659  ectocld  6742  ecoptocl  6764  mapsn  6825  eqeng  6911  difsnen  6960  fopwdom  6986  frfi  7118  elfiun  7199  ordiso  7247  ordtypelem7  7255  wemaplem2  7278  suc11reg  7336  inf3lem6  7350  noinfep  7376  cantnff  7391  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnflem1  7407  cantnf  7411  r111  7463  rankc2  7559  tcrank  7570  cardnueq0  7613  fodomfi2  7703  alephinit  7738  dfac9  7778  dfac12k  7789  cdainf  7834  ackbij1  7880  ackbij2  7885  sornom  7919  fin23lem16  7977  fin23lem21  7981  isf32lem2  7996  fin1a2lem6  8047  itunitc  8063  zorn2lem4  8142  wunr1om  8357  tskr1om  8405  recmulnq  8604  ltexnq  8615  distrlem4pr  8666  1re  8853  0re  8854  0cnALT  9057  mulge0  9307  prodgt0  9617  peano2nn  9774  recnz  10103  zneo  10110  uzn0  10259  xlemul1a  10624  prunioo  10780  flidz  10957  modid2  11010  om2uzrani  11031  uzrdgfni  11037  seqid  11107  seqz  11110  facdiv  11316  facwordi  11318  hashdom  11377  sqrmo  11753  fsumf1o  12212  isumltss  12323  supcvg  12330  dvdsnegb  12562  odd2np1lem  12602  odd2np1  12603  bitsuz  12681  bezoutlem4  12736  gcddiv  12744  gcdeq  12747  dvdssqim  12748  dvdsprm  12794  coprm  12795  coprmdvds2  12798  prmdvdsexp  12809  rpmul  12818  prmdiv  12869  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pythagtriplem19  12902  pc2dvds  12947  pcadd  12953  prmpwdvds  12967  vdwlem11  13054  ramubcl  13081  0ram  13083  mreexexd  13566  posasymb  14102  pleval2  14115  pltval3  14117  plttr  14120  pospo  14123  letsr  14365  ismgmid  14403  imasmnd2  14425  isgrpid2  14534  isgrpinv  14548  imasgrp2  14626  orbsta  14783  odmulg  14885  odmulgeq  14886  gexdvdsi  14910  gexnnod  14915  pgpssslw  14941  sylow2alem1  14944  fislw  14952  lsmss1b  14992  lsmss2b  14994  efgrelexlemb  15075  torsubg  15162  ablfacrplem  15316  pgpfac1lem2  15326  pgpfac1lem3  15328  imasrng  15418  dvdsrcl2  15448  dvdsrtr  15450  dvdsrmul1  15451  irredn0  15501  lspsneq0  15785  lmhmima  15820  lspsolv  15912  opsrtoslem2  16242  xrsdsreclblem  16433  dvdsrz  16456  prmirredlem  16462  znunit  16533  pjdm2  16627  obselocv  16644  baspartn  16708  bastop  16735  iscld3  16817  isopn3  16819  iscldtop  16848  ordtrest2lem  16949  2ndcredom  17192  2ndc1stc  17193  2ndcrest  17196  2ndcdisj  17198  2ndcsep  17201  kgenidm  17258  dfac14  17328  tx2ndc  17361  kqreglem1  17448  rnelfm  17664  fmfnfmlem2  17666  fmfnfmlem4  17668  fmfnfm  17669  flimtopon  17681  fclstopon  17723  xrsmopn  18334  icccmplem2  18344  reconnlem1  18347  iccpnfcnv  18458  cphsqrcl2  18638  ivthlem3  18829  ivthicc  18834  ovolctb  18865  ioombl  18938  itgabs  19205  itgsplitioo  19208  dvlip  19356  c1liplem1  19359  c1lip1  19360  dvgt0lem1  19365  dvivthlem2  19372  dvne0  19374  lhop1lem  19376  lhop1  19377  lhop2  19378  lhop  19379  dvcvx  19383  itgsubstlem  19411  mpfind  19444  mpfpf1  19450  pf1mpf  19451  mdegnn0cl  19473  ig1peu  19573  elply2  19594  plypf1  19610  dgreq0  19662  aannenlem3  19726  abelthlem2  19824  lognegb  19959  eflogeq  19971  efopn  20021  cxpge0  20046  cxplea  20059  cxple2  20060  cxpcn3lem  20103  cxpaddlelem  20107  cxpaddle  20108  cxpeq  20113  asinsinb  20209  acoscosb  20210  atantanb  20236  leibpilem1  20252  wilthlem2  20323  sqf11  20393  sqff1o  20436  ppiublem1  20457  lgsdir  20585  lgsne0  20588  lgsquadlem3  20611  2sqblem  20632  dchrisum0flblem1  20673  ostth3  20803  ostth  20804  isgrp2d  20918  rngosn3  21109  htthlem  21513  pjpreeq  21993  h1dn0  22147  spansneleqi  22164  rnbra  22703  dfpjop  22778  elpjrn  22786  stm1i  22839  mdbr2  22892  mdsl2i  22918  sumdmdlem  23014  dmdbr6ati  23019  xrge0iifcnv  23330  erdszelem8  23744  cvmlift3lem4  23868  cvmlift3lem5  23869  umgraf  23885  eupath2lem2  23917  eupath2lem3  23918  ghomgrpilem2  24008  dvdspw  24174  dfon2lem9  24218  poseq  24324  nodenselem3  24408  nodenselem5  24410  nodenselem8  24413  nofulllem5  24431  colinearalg  24610  axcontlem5  24668  axcontlem9  24672  btwnconn1lem11  24792  broutsideof2  24817  itgabsnc  25020  twsymr  25181  apnei  25623  fil2ss  25660  fnctartar  26010  fnctartar2  26011  opnbnd  26346  tailfb  26429  sdclem2  26555  subspopn  26569  equivtotbnd  26605  igenval2  26794  isfldidl  26796  ismrc  26879  pellexlem1  27017  aomclem4  27257  dfac21  27267  lsmfgcl  27275  lmhmfgima  27285  dfacbasgrp  27376  lindfrn  27394  hbtlem6  27436  pmtrfrn  27503  fiuneneq  27616  xrltneNEW  27760  stoweidlem27  27879  stoweidlem29  27881  usgrcyclnl1  28386  nvnencycllem  28389  lshpinN  29801  lsatcv0eq  29859  lsatcv1  29860  cvrnbtwn3  30088  cvrnbtwn4  30091  cvrcmp  30095  atnlt  30125  cvlexchb1  30142  2llnne2N  30219  atcvr0eq  30237  lnnat  30238  cvrat4  30254  ps-1  30288  3at  30301  llncmp  30333  llnnlt  30334  llncvrlpln2  30368  llncvrlpln  30369  lplncmp  30373  lplnnlt  30376  lplncvrlvol2  30426  lplncvrlvol  30427  lvolcmp  30428  lvolnltN  30429  dalempnes  30462  dalemqnet  30463  dalem-cly  30482  dalem44  30527  lncmp  30594  cdlemblem  30604  llnexch2N  30681  osumcllem4N  30770  pexmidlem1N  30781  lhp2atnle  30844  cdleme11dN  31073  cdleme20k  31130  cdleme21at  31139  cdleme21ct  31140  cdleme32e  31256  cdleme35f  31265  tendoex  31786  dochexmidlem1  32272  lcfrlem9  32362  mapd1o  32460  mapdindp3  32534
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