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

Theorem syl6ib 160
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ib.1  |-  ( ph  ->  ( ps  ->  ch ) )
syl6ib.2  |-  ( ch  <->  th )
Assertion
Ref Expression
syl6ib  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem syl6ib
StepHypRef Expression
1 syl6ib.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 syl6ib.2 . . 3  |-  ( ch  <->  th )
32biimpi 119 . 2  |-  ( ch 
->  th )
41, 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:  3imtr3g  203  exp4a  363  con2biddc  865  nfalt  1557  alexim  1624  19.36-1  1651  ax11ev  1800  equs5or  1802  necon2bd  2364  necon2d  2365  necon1bbiddc  2369  necon2abiddc  2372  necon2bbiddc  2373  necon4idc  2375  necon4ddc  2378  necon1bddc  2383  spc2gv  2771  spc3gv  2773  mo2icl  2858  reupick  3355  prneimg  3696  invdisj  3918  trin  4031  exmidsssnc  4121  ordsucss  4415  eqbrrdva  4704  elreldm  4760  elres  4850  xp11m  4972  ssrnres  4976  opelf  5289  dffo4  5561  dftpos3  6152  tfr1onlemaccex  6238  tfrcllemaccex  6251  nnaordex  6416  swoer  6450  map0g  6575  mapsn  6577  nneneq  6744  fnfi  6818  prarloclemlo  7295  genprndl  7322  genprndu  7323  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  caucvgsrlemoffres  7601  caucvgsr  7603  nntopi  7695  letr  7840  reapcotr  8353  apcotr  8362  mulext1  8367  cnstab  8400  lt2msq  8637  nneoor  9146  xrletr  9584  icoshft  9766  caucvgre  10746  absext  10828  rexico  10986  summodc  11145  gcdeq0  11654  tgcn  12366  cnptoprest  12397  metequiv2  12654  bj-nnsn  12934  bj-inf2vnlem2  13158
  Copyright terms: Public domain W3C validator