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

Theorem syl6ibr 155
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ibr.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6ibr.2  |-  ( th  <->  ch )
Assertion
Ref Expression
syl6ibr  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6ibr.2 . . 3  |-  ( th  <->  ch )
32biimpri 128 . 2  |-  ( ch 
->  th )
41, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr4g  198  imp4a  335  dcbi  855  oplem1  893  3impexpbicom  1343  hband  1394  hb3and  1395  nfand  1476  nfimd  1493  equsexd  1633  euim  1984  mopick2  1999  2moswapdc  2006  necon3bd  2263  necon3d  2264  necon2ad  2277  necon1abiddc  2282  ralrimd  2414  rspcimedv  2675  2reuswapdc  2765  ra5  2873  difin  3201  r19.2m  3336  tpid3g  3510  sssnm  3552  ssiun  3726  ssiun2  3727  sotricim  4087  sotritrieq  4089  tron  4146  ordsucss  4257  ordunisuc2r  4267  ordpwsucss  4318  dmcosseq  4630  relssres  4675  trin2  4743  ssrnres  4790  fnun  5032  f1oun  5173  ssimaex  5261  chfnrn  5305  dffo4  5342  dffo5  5343  isoselem  5486  fnoprabg  5629  poxp  5880  issmo2  5934  smores  5937  tfr0  5967  tfrlemibxssdm  5971  swoer  6164  qsss  6195  findcard  6375  findcard2  6376  findcard2s  6377  supmoti  6398  indpi  6497  recexprlemm  6779  recexprlemloc  6786  recexprlem1ssl  6788  recexprlem1ssu  6789  recexprlemss1l  6790  recexprlemss1u  6791  zmulcl  8354  indstr  8631  eluzdc  8643  icoshft  8958  fzouzsplit  9136  dvds2lem  10112  oddnn02np1  10184  sqrt2irr  10223  bj-omssind  10418  bj-om  10420  bj-inf2vnlem3  10456  bj-inf2vnlem4  10457
  Copyright terms: Public domain W3C validator