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  1820  gencl  2718  spsbc  2920  prexg  4133  posng  4611  sosng  4612  optocl  4615  relcnvexb  5078  funimass1  5200  dmfex  5312  f1ocnvb  5381  eqfnfv2  5519  elpreima  5539  dff13  5669  f1ocnvfv  5680  f1ocnvfvb  5681  fliftfun  5697  eusvobj2  5760  mpoxopn0yelv  6136  rntpos  6154  erexb  6454  findcard2  6783  findcard2s  6784  xpfi  6818  sbthlemi3  6847  enq0tr  7256  addnqprllem  7349  addnqprulem  7350  distrlem1prl  7404  distrlem1pru  7405  recexprlem1ssl  7455  recexprlem1ssu  7456  elrealeu  7651  addcan  7956  addcan2  7957  neg11  8027  negreb  8041  mulcanapd  8436  receuap  8444  cju  8733  nn1suc  8753  nnaddcl  8754  nndivtr  8776  znegclb  9101  zaddcllempos  9105  zmulcl  9121  zeo  9170  uz11  9362  uzp1  9373  eqreznegel  9420  xneg11  9631  xnegdi  9665  modqadd1  10148  modqmul1  10164  frec2uzltd  10190  bccmpl  10514  fz1eqb  10551  cj11  10691  rennim  10788  resqrexlemgt0  10806  efne0  11398  dvdsabseq  11558  uptx  12459  hmeocnvb  12503  tgioo  12731  bj-nnbidc  13069  bj-prexg  13216  strcollnft  13289
  Copyright terms: Public domain W3C validator