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  2837  rmob  2973  preqr1g  3663  issod  4211  sotritrieq  4217  nsuceq0g  4310  suctr  4313  nordeq  4429  suc11g  4442  iss  4835  poirr2  4901  xp11m  4947  tz6.12c  5419  fnbrfvb  5430  fvelimab  5445  foeqcnvco  5659  f1eqcocnv  5660  acexmidlemcase  5737  nna0r  6342  nnawordex  6392  ectocld  6463  ecoptocl  6484  mapsn  6552  eqeng  6628  fopwdom  6698  ordiso  6889  ltexnqq  7184  nsmallnqq  7188  nqprloc  7321  aptiprleml  7415  map2psrprg  7581  0re  7734  lttri3  7812  0cnALT  7920  reapti  8309  recnz  9112  zneo  9120  uzn0  9309  flqidz  10027  ceilqidz  10057  modqid2  10092  modqmuladdnn0  10109  frec2uzrand  10146  frecuzrdgtcl  10153  seq3id  10249  seq3z  10252  facdiv  10452  facwordi  10454  maxleb  10956  fsumf1o  11127  dvdsnegb  11437  odd2np1lem  11496  odd2np1  11497  ltoddhalfle  11517  halfleoddlt  11518  opoe  11519  omoe  11520  opeo  11521  omeo  11522  gcddiv  11634  gcdzeq  11637  dvdssqim  11639  lcmgcdeq  11691  coprmdvds2  11701  rpmul  11706  divgcdcoprmex  11710  cncongr2  11712  dvdsprm  11744  coprm  11749  prmdvdsexp  11753  exmidunben  11866  baspartn  12144  bastop  12171  isopn3  12221  bj-peano4  13080  sbthomlem  13147
  Copyright terms: Public domain W3C validator