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

Theorem syl6ibr 160
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 131 . 2  |-  ( ch 
->  th )
41, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr4g  203  imp4a  341  dcbi  878  oplem1  917  3impexpbicom  1368  hband  1419  hb3and  1420  nfand  1501  nfimd  1518  equsexd  1659  euim  2011  mopick2  2026  2moswapdc  2033  necon3bd  2292  necon3d  2293  necon2ad  2306  necon1abiddc  2311  ralrimd  2444  rspcimedv  2712  2reuswapdc  2803  ra5  2911  difin  3217  r19.2m  3345  tpid3g  3523  sssnm  3566  ssiun  3740  ssiun2  3741  sotricim  4106  sotritrieq  4108  tron  4165  ordsucss  4276  ordunisuc2r  4286  ordpwsucss  4338  dmcosseq  4651  relssres  4696  trin2  4766  ssrnres  4813  fnun  5056  f1oun  5197  ssimaex  5286  chfnrn  5330  dffo4  5367  dffo5  5368  isoselem  5510  fnoprabg  5653  poxp  5904  issmo2  5958  smores  5961  tfr0dm  5991  tfrlemibxssdm  5996  tfr1onlembxssdm  6012  tfrcllembxssdm  6025  swoer  6221  qsss  6252  findcard  6444  findcard2  6445  findcard2s  6446  supmoti  6500  pm54.43  6570  indpi  6646  recexprlemm  6928  recexprlemloc  6935  recexprlem1ssl  6937  recexprlem1ssu  6938  recexprlemss1l  6939  recexprlemss1u  6940  zmulcl  8537  indstr  8814  eluzdc  8830  icoshft  9140  fzouzsplit  9317  hashunlem  9880  dvds2lem  10415  oddnn02np1  10487  dfgcd2  10610  sqrt2irr  10748  decidr  10866  bj-omssind  10997  bj-om  10999  bj-inf2vnlem3  11034  bj-inf2vnlem4  11035
  Copyright terms: Public domain W3C validator