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

Theorem syl5ibcom 153
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 152 . 2  |-  ( ch 
->  ( ph  ->  th )
)
43com12 30 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biimpcd  157  mob2  2773  rmob  2907  preqr1g  3566  issod  4082  sotritrieq  4088  nsuceq0g  4181  suctr  4184  nordeq  4295  suc11g  4308  iss  4684  poirr2  4747  xp11m  4789  tz6.12c  5235  fnbrfvb  5246  fvelimab  5261  foeqcnvco  5461  f1eqcocnv  5462  acexmidlemcase  5538  nna0r  6122  nnawordex  6167  ectocld  6238  ecoptocl  6259  eqeng  6313  fopwdom  6380  ordiso  6506  ltexnqq  6660  nsmallnqq  6664  nqprloc  6797  aptiprleml  6891  0re  7181  lttri3  7258  0cnALT  7365  reapti  7746  recnz  8521  zneo  8529  uzn0  8715  flqidz  9368  ceilqidz  9398  modqid2  9433  modqmuladdnn0  9450  frec2uzrand  9487  frecuzrdgtcl  9494  iseqid  9563  iseqz  9566  facdiv  9762  facwordi  9764  maxleb  10240  dvdsnegb  10357  odd2np1lem  10416  odd2np1  10417  ltoddhalfle  10437  halfleoddlt  10438  opoe  10439  omoe  10440  opeo  10441  omeo  10442  gcddiv  10552  gcdzeq  10555  dvdssqim  10557  lcmgcdeq  10609  coprmdvds2  10619  rpmul  10624  divgcdcoprmex  10628  cncongr2  10630  dvdsprm  10662  coprm  10667  prmdvdsexp  10671  bj-peano4  10908
  Copyright terms: Public domain W3C validator