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

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

Proof of Theorem syl6bi
StepHypRef Expression
1 syl6bi.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimpd 143 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 syl6bi.2 . 2  |-  ( ch 
->  th )
42, 3syl6 33 1  |-  ( ph  ->  ( ps  ->  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:  19.33bdc  1609  ax11i  1692  equveli  1732  eupickbi  2079  rgen2a  2484  reu6  2868  sseq0  3399  disjel  3412  preq12b  3692  prel12  3693  prneimg  3696  elinti  3775  exmidundif  4124  opthreg  4466  elreldm  4760  issref  4916  relcnvtr  5053  relresfld  5063  funopg  5152  funimass2  5196  f0dom0  5311  fvimacnv  5528  elunirn  5660  oprabid  5796  op1steq  6070  f1o2ndf1  6118  reldmtpos  6143  rntpos  6147  nntri3or  6382  nnaordex  6416  nnawordex  6417  findcard2  6776  findcard2s  6777  mkvprop  7025  lt2addnq  7205  lt2mulnq  7206  genpelvl  7313  genpelvu  7314  distrlem5prl  7387  distrlem5pru  7388  caucvgprlemnkj  7467  map2psrprg  7606  rereceu  7690  ltxrlt  7823  0mnnnnn0  9002  elnnnn0b  9014  nn0le2is012  9126  btwnz  9163  uz11  9341  nn01to3  9402  zq  9411  xrltso  9575  xltnegi  9611  xnn0lenn0nn0  9641  xnn0xadd0  9643  iccleub  9707  fzdcel  9813  uznfz  9876  2ffzeq  9911  elfzonlteqm1  9980  flqeqceilz  10084  modqadd1  10127  modqmul1  10143  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  fzfig  10196  m1expeven  10333  caucvgrelemcau  10745  rexico  10986  fisumss  11154  fsum2dlemstep  11196  ntrivcvgap  11310  0dvds  11498  alzdvds  11537  opoe  11577  omoe  11578  opeo  11579  omeo  11580  m1exp1  11583  nn0enne  11584  nn0o1gt2  11587  gcdneg  11655  dfgcd2  11687  algcvgblem  11715  algcvga  11717  eucalglt  11723  coprmdvds  11758  divgcdcoprmex  11768  cncongr1  11769  prm2orodd  11792  tg2  12214  tgcl  12218  neii1  12301  neii2  12303  txlm  12433  reopnap  12692  tgioo  12700  addcncntoplem  12705  bj-elssuniab  12983  bj-nn0sucALT  13161  triap  13209
  Copyright terms: Public domain W3C validator