ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5ibcom Unicode version

Theorem syl5ibcom 154
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 153 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biimpcd  158  mob2  2835  rmob  2971  preqr1g  3661  issod  4209  sotritrieq  4215  nsuceq0g  4308  suctr  4311  nordeq  4427  suc11g  4440  iss  4833  poirr2  4899  xp11m  4945  tz6.12c  5417  fnbrfvb  5428  fvelimab  5443  foeqcnvco  5657  f1eqcocnv  5658  acexmidlemcase  5735  nna0r  6340  nnawordex  6390  ectocld  6461  ecoptocl  6482  mapsn  6550  eqeng  6626  fopwdom  6696  ordiso  6887  ltexnqq  7180  nsmallnqq  7184  nqprloc  7317  aptiprleml  7411  map2psrprg  7577  0re  7730  lttri3  7808  0cnALT  7916  reapti  8304  recnz  9098  zneo  9106  uzn0  9293  flqidz  10010  ceilqidz  10040  modqid2  10075  modqmuladdnn0  10092  frec2uzrand  10129  frecuzrdgtcl  10136  seq3id  10232  seq3z  10235  facdiv  10435  facwordi  10437  maxleb  10939  fsumf1o  11110  dvdsnegb  11417  odd2np1lem  11476  odd2np1  11477  ltoddhalfle  11497  halfleoddlt  11498  opoe  11499  omoe  11500  opeo  11501  omeo  11502  gcddiv  11614  gcdzeq  11617  dvdssqim  11619  lcmgcdeq  11671  coprmdvds2  11681  rpmul  11686  divgcdcoprmex  11690  cncongr2  11692  dvdsprm  11724  coprm  11729  prmdvdsexp  11733  exmidunben  11845  baspartn  12123  bastop  12150  isopn3  12200  bj-peano4  12987  sbthomlem  13054
  Copyright terms: Public domain W3C validator