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

Theorem syl5ib 152
Description: A mixed syllogism inference. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5ib.1  |-  ( ph  ->  ps )
syl5ib.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
syl5ib  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem syl5ib
StepHypRef Expression
1 syl5ib.1 . 2  |-  ( ph  ->  ps )
2 syl5ib.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32biimpd 142 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  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:  syl5ibcom  153  syl5ibr  154  sbft  1770  gencl  2632  spsbc  2827  prexg  3968  posng  4432  sosng  4433  optocl  4436  relcnvexb  4881  funimass1  5001  dmfex  5104  f1ocnvb  5165  eqfnfv2  5292  elpreima  5312  dff13  5433  f1ocnvfv  5444  f1ocnvfvb  5445  fliftfun  5461  eusvobj2  5523  mpt2xopn0yelv  5882  rntpos  5900  erexb  6190  findcard2  6413  findcard2s  6414  enq0tr  6675  addnqprllem  6768  addnqprulem  6769  distrlem1prl  6823  distrlem1pru  6824  recexprlem1ssl  6874  recexprlem1ssu  6875  elrealeu  7049  addcan  7344  addcan2  7345  neg11  7415  negreb  7429  mulcanapd  7807  receuap  7815  cju  8094  nn1suc  8114  nnaddcl  8115  nndivtr  8136  znegclb  8454  zaddcllempos  8458  zmulcl  8474  zeo  8522  uz11  8711  uzp1  8722  eqreznegel  8769  xneg11  8966  modqadd1  9432  modqmul1  9448  frec2uzltd  9474  bccmpl  9767  fz1eqb  9804  cj11  9919  rennim  10015  resqrexlemgt0  10033  dvdsabseq  10381  bj-prexg  10845  strcollnft  10922
  Copyright terms: Public domain W3C validator