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

Theorem syl5ib 153
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 143 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  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:  syl5ibcom  154  syl5ibr  155  sbft  1804  gencl  2692  spsbc  2893  prexg  4103  posng  4581  sosng  4582  optocl  4585  relcnvexb  5048  funimass1  5170  dmfex  5282  f1ocnvb  5349  eqfnfv2  5487  elpreima  5507  dff13  5637  f1ocnvfv  5648  f1ocnvfvb  5649  fliftfun  5665  eusvobj2  5728  mpoxopn0yelv  6104  rntpos  6122  erexb  6422  findcard2  6751  findcard2s  6752  xpfi  6786  sbthlemi3  6815  enq0tr  7210  addnqprllem  7303  addnqprulem  7304  distrlem1prl  7358  distrlem1pru  7359  recexprlem1ssl  7409  recexprlem1ssu  7410  elrealeu  7605  addcan  7910  addcan2  7911  neg11  7981  negreb  7995  mulcanapd  8390  receuap  8398  cju  8687  nn1suc  8707  nnaddcl  8708  nndivtr  8730  znegclb  9055  zaddcllempos  9059  zmulcl  9075  zeo  9124  uz11  9316  uzp1  9327  eqreznegel  9374  xneg11  9585  xnegdi  9619  modqadd1  10102  modqmul1  10118  frec2uzltd  10144  bccmpl  10468  fz1eqb  10505  cj11  10645  rennim  10742  resqrexlemgt0  10760  efne0  11311  dvdsabseq  11472  uptx  12370  hmeocnvb  12414  tgioo  12642  bj-nnbidc  12889  bj-prexg  13036  strcollnft  13109
  Copyright terms: Public domain W3C validator