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  8389  receuap  8397  cju  8683  nn1suc  8703  nnaddcl  8704  nndivtr  8726  znegclb  9045  zaddcllempos  9049  zmulcl  9065  zeo  9114  uz11  9304  uzp1  9315  eqreznegel  9362  xneg11  9572  xnegdi  9606  modqadd1  10089  modqmul1  10105  frec2uzltd  10131  bccmpl  10455  fz1eqb  10492  cj11  10632  rennim  10729  resqrexlemgt0  10747  efne0  11298  dvdsabseq  11457  uptx  12354  hmeocnvb  12398  tgioo  12626  bj-nnbidc  12858  bj-prexg  13005  strcollnft  13078
  Copyright terms: Public domain W3C validator