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  882  oplem1  921  3impexpbicom  1372  hband  1423  hb3and  1424  nfand  1505  nfimd  1522  equsexd  1664  euim  2016  mopick2  2031  2moswapdc  2038  necon3bd  2298  necon3d  2299  necon2ad  2312  necon1abiddc  2317  ralrimd  2451  rspcimedv  2724  2reuswapdc  2817  ra5  2925  difin  3234  r19.2m  3365  tpid3g  3550  sssnm  3593  ssiun  3767  ssiun2  3768  disjnim  3828  sotricim  4141  sotritrieq  4143  tron  4200  ordsucss  4311  ordunisuc2r  4321  ordpwsucss  4373  dmcosseq  4692  relssres  4737  trin2  4810  ssrnres  4860  fnun  5106  f1oun  5257  ssimaex  5349  chfnrn  5394  dffo4  5431  dffo5  5432  isoselem  5581  fnoprabg  5728  poxp  5979  issmo2  6036  smores  6039  tfr0dm  6069  tfrlemibxssdm  6074  tfr1onlembxssdm  6090  tfrcllembxssdm  6103  swoer  6300  qsss  6331  findcard  6584  findcard2  6585  findcard2s  6586  supmoti  6667  pm54.43  6797  indpi  6880  recexprlemm  7162  recexprlemloc  7169  recexprlem1ssl  7171  recexprlem1ssu  7172  recexprlemss1l  7173  recexprlemss1u  7174  zmulcl  8773  indstr  9050  eluzdc  9066  icoshft  9376  fzouzsplit  9555  hashunlem  10177  modfsummod  10815  dvds2lem  10901  oddnn02np1  10973  dfgcd2  11096  sqrt2irr  11234  decidr  11353  bj-omssind  11487  bj-om  11489  bj-inf2vnlem3  11524  bj-inf2vnlem4  11525
  Copyright terms: Public domain W3C validator