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

Theorem imbitrid 154
Description: A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)
Hypotheses
Ref Expression
imbitrid.1  |-  ( ph  ->  ps )
imbitrid.2  |-  ( ch 
->  ( ps  <->  th )
)
Assertion
Ref Expression
imbitrid  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem imbitrid
StepHypRef Expression
1 imbitrid.1 . 2  |-  ( ph  ->  ps )
2 imbitrid.2 . . 3  |-  ( ch 
->  ( ps  <->  th )
)
32biimpd 144 . 2  |-  ( ch 
->  ( ps  ->  th )
)
41, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  syl5ibcom  155  imbitrrid  156  sbft  1848  gencl  2771  spsbc  2976  prexg  4213  posng  4700  sosng  4701  optocl  4704  relcnvexb  5170  funimass1  5295  dmfex  5407  f1ocnvb  5477  eqfnfv2  5616  elpreima  5637  dff13  5771  f1ocnvfv  5782  f1ocnvfvb  5783  fliftfun  5799  eusvobj2  5863  mpoxopn0yelv  6242  rntpos  6260  erexb  6562  findcard2  6891  findcard2s  6892  xpfi  6931  sbthlemi3  6960  enq0tr  7435  addnqprllem  7528  addnqprulem  7529  distrlem1prl  7583  distrlem1pru  7584  recexprlem1ssl  7634  recexprlem1ssu  7635  elrealeu  7830  addcan  8139  addcan2  8140  neg11  8210  negreb  8224  mulcanapd  8620  receuap  8628  cju  8920  nn1suc  8940  nnaddcl  8941  nndivtr  8963  znegclb  9288  zaddcllempos  9292  zmulcl  9308  zeo  9360  uz11  9552  uzp1  9563  eqreznegel  9616  xneg11  9836  xnegdi  9870  modqadd1  10363  modqmul1  10379  frec2uzltd  10405  bccmpl  10736  fz1eqb  10772  cj11  10916  rennim  11013  resqrexlemgt0  11031  efne0  11688  dvdsabseq  11855  pcfac  12350  grpinveu  12916  mulgass  13025  dvreq1  13316  uptx  13813  hmeocnvb  13857  tgioo  14085  bj-nnbidc  14548  bj-prexg  14702  strcollnft  14775
  Copyright terms: Public domain W3C validator