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

Theorem syl5ibcom 224
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 223 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 33 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188
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 189
This theorem is referenced by:  biimpcd  228  mob2  3252  rmob  3393  disjxun  4420  sotric  4799  sotrieq  4800  iss  5170  poirr2  5242  xp11  5290  nordeq  5460  nsuceq0  5521  suctr  5524  tz6.12c  5899  fnbrfvb  5920  foeqcnvco  6212  f1eqcocnv  6213  dfwe2  6621  mpt2sn  6897  tfrlem15  7120  tz7.44-2  7135  tz7.48-1  7170  tz7.49  7172  oawordexr  7267  oewordi  7302  oeeulem  7312  nna0r  7320  nnawordex  7348  nnaordex  7349  oaabs  7355  oaabs2  7356  ectocld  7440  ecoptocl  7463  mapsn  7523  eqeng  7612  difsnen  7662  fopwdom  7688  frfi  7824  elfiun  7952  ordiso  8039  ordtypelem7  8047  wemaplem2  8070  suc11reg  8132  inf3lem6  8146  noinfep  8172  cantnff  8186  cantnfp1lem2  8191  cantnfp1lem3  8192  cantnflem1  8201  cantnf  8205  r111  8253  rankc2  8349  tcrank  8362  cardnueq0  8405  fodomfi2  8497  alephinit  8532  dfac9  8572  dfac12k  8583  cdainf  8628  ackbij1  8674  ackbij2  8679  sornom  8713  fin23lem16  8771  fin23lem21  8775  isf32lem2  8790  fin1a2lem6  8841  itunitc  8857  zorn2lem4  8935  wunr1om  9150  tskr1om  9198  recmulnq  9395  ltexnq  9406  distrlem4pr  9457  1re  9648  0re  9649  0cnALT  9870  mulge0  10138  prodgt0  10456  peano2nn  10627  recnz  11017  zneo  11024  uzn0  11180  xlemul1a  11580  prunioo  11767  flidz  12051  ceilidz  12084  modid2  12129  om2uzrani  12171  uzrdgfni  12177  seqid  12263  seqz  12266  facdiv  12477  facwordi  12479  hashdom  12563  wrdnval  12699  wrdl1s1  12751  sqrmo  13313  fsumf1o  13786  isumltss  13903  supcvg  13911  dvdsnegb  14317  odd2np1lem  14361  odd2np1  14362  bitsuz  14445  bezoutlem4OLD  14503  bezoutlem4  14506  gcddiv  14514  gcdeq  14517  dvdssqim  14518  lcmgcdeq  14574  dvdsprm  14644  coprm  14654  coprmdvds2  14657  prmdvdsexp  14664  rpmul  14672  prmdiv  14730  opoe  14758  omoe  14759  opeo  14760  omeo  14761  pythagtriplem19  14780  pc2dvds  14825  pcadd  14831  prmpwdvds  14845  vdwlem11  14938  ramubcl  14973  0ram  14975  mreexexd  15551  posasymb  16195  pleval2  16208  pltval3  16210  plttr  16213  pospo  16216  letsr  16470  intopsn  16495  ismgmid  16504  imasmnd2  16570  isgrpid2  16699  isgrpinv  16713  imasgrp2  16798  orbsta  16964  symgfix2  17054  pmtrfrn  17096  pmtrrn2  17098  odmulg  17204  odmulgeq  17205  gexdvdsi  17231  gexnnod  17237  pgpssslw  17263  sylow2alem1  17266  fislw  17274  lsmss1b  17314  lsmss2b  17316  efgrelexlemb  17397  torsubg  17489  ablfacrplem  17695  pgpfac1lem2  17705  pgpfac1lem3  17707  imasring  17844  dvdsrcl2  17875  dvdsrtr  17877  dvdsrmul1  17878  irredn0  17928  lspsneq0  18232  lmhmima  18267  lspsolv  18363  opsrtoslem2  18705  mpfind  18756  mpfpf1  18936  pf1mpf  18937  xrsdsreclblem  19011  dvdsrzring  19048  prmirredlem  19060  znunit  19130  pjdm2  19270  obselocv  19287  lindfrn  19375  cpmadugsumlemF  19896  baspartn  19965  bastop  19993  iscld3  20076  isopn3  20078  iscldtop  20107  ordtrest2lem  20215  2ndcredom  20461  2ndc1stc  20462  2ndcrest  20465  2ndcdisj  20467  2ndcsep  20470  kgenidm  20558  dfac14  20629  tx2ndc  20662  kqreglem1  20752  rnelfm  20964  fmfnfmlem2  20966  fmfnfmlem4  20968  fmfnfm  20969  flimtopon  20981  fclstopon  21023  xrsmopn  21826  icccmplem2  21837  reconnlem1  21840  iccpnfcnv  21968  cphsqrtcl2  22160  ivthlem3  22400  ivthicc  22405  ovolctb  22439  ioombl  22514  itgabs  22788  itgsplitioo  22791  dvlip  22941  c1liplem1  22944  c1lip1  22945  dvgt0lem1  22950  dvivthlem2  22957  dvne0  22959  lhop1lem  22961  lhop1  22962  lhop2  22963  lhop  22964  dvcvx  22968  itgsubstlem  22996  mdegnn0cl  23016  ig1peu  23118  ig1peuOLD  23119  elply2  23146  plypf1  23162  dgreq0  23215  aannenlem3  23282  abelthlem2  23383  lognegb  23535  eflogeq  23547  efopn  23599  cxpge0  23624  cxplea  23637  cxple2  23638  cxpcn3lem  23683  cxpaddlelem  23687  cxpaddle  23688  cxpeq  23693  asinsinb  23819  acoscosb  23820  atantanb  23846  leibpilem1  23862  wilthlem2  23990  sqf11  24062  sqff1o  24105  ppiublem1  24126  lgsdir  24254  lgsne0  24257  lgsquadlem3  24280  2sqblem  24301  dchrisum0flblem1  24342  ostth3  24472  ostth  24473  colinearalg  24936  axcontlem5  24994  axcontlem9  24998  umgraf  25041  uslgraf1oedg  25082  nbgrassvwo  25161  usgrcyclnl1  25364  nvnencycllem  25367  clwwlknprop  25496  clwlkf1clwwlklem1  25570  usg2wlkonot  25607  usg2wotspth  25608  eupath2lem2  25702  eupath2lem3  25703  isgrp2d  25959  rngosn3  26150  htthlem  26566  pjpreeq  27047  h1dn0  27201  spansneleqi  27218  rnbra  27756  dfpjop  27831  elpjrn  27839  stm1i  27892  mdbr2  27945  mdsl2i  27971  sumdmdlem  28067  dmdbr6ati  28072  ordtrest2NEWlem  28734  xrge0iifcnv  28745  eulerpartlemb  29207  erdszelem8  29927  cvmlift3lem4  30051  cvmlift3lem5  30052  mrsub0  30160  mrsubccat  30162  mrsubcn  30163  msubrn  30173  msrid  30189  elmthm  30220  ghomgrpilem2  30310  dvdspw  30391  dfon2lem9  30442  poseq  30496  nodenselem3  30575  nodenselem5  30577  nodenselem8  30580  nofulllem5  30598  btwnconn1lem11  30867  broutsideof2  30892  opnbnd  30984  tailfb  31036  fin2so  31894  poimirlem9  31911  poimirlem17  31919  poimirlem26  31928  poimirlem27  31929  poimirlem31  31933  itgabsnc  31973  ftc2nc  31988  sdclem2  32033  subspopn  32043  equivtotbnd  32072  igenval2  32261  isfldidl  32263  lshpinN  32522  lsatcv0eq  32580  lsatcv1  32581  cvrnbtwn3  32809  cvrnbtwn4  32812  cvrcmp  32816  atnlt  32846  cvlexchb1  32863  2llnne2N  32940  atcvr0eq  32958  lnnat  32959  cvrat4  32975  ps-1  33009  3at  33022  llncmp  33054  llnnlt  33055  llncvrlpln2  33089  llncvrlpln  33090  lplncmp  33094  lplnnlt  33097  lplncvrlvol2  33147  lplncvrlvol  33148  lvolcmp  33149  lvolnltN  33150  dalempnes  33183  dalemqnet  33184  dalem-cly  33203  dalem44  33248  lncmp  33315  cdlemblem  33325  llnexch2N  33402  osumcllem4N  33491  pexmidlem1N  33502  lhp2atnle  33565  cdleme11dN  33795  cdleme20k  33853  cdleme21at  33862  cdleme21ct  33863  cdleme32e  33979  cdleme35f  33988  tendoex  34509  dochexmidlem1  34995  lcfrlem9  35085  mapd1o  35183  mapdindp3  35257  ismrc  35510  pellexlem1  35641  aomclem4  35883  dfac21  35892  lsmfgcl  35900  lmhmfgima  35910  dfacbasgrp  35935  hbtlem6  35956  fiuneneq  36039  stoweidlem27  37755  stoweidlem29  37757  stoweidlem29OLD  37758  iccpartrn  38504  gcdzeq  38553  umgrf  38892  uspgrf1oedg  38941  assintopass  39242
  Copyright terms: Public domain W3C validator