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  850  nfalt  1542  alexim  1609  19.36-1  1636  ax11ev  1784  equs5or  1786  necon2bd  2343  necon2d  2344  necon1bbiddc  2348  necon2abiddc  2351  necon2bbiddc  2352  necon4idc  2354  necon4ddc  2357  necon1bddc  2362  spc2gv  2750  spc3gv  2752  mo2icl  2836  reupick  3330  prneimg  3671  invdisj  3893  trin  4006  exmidsssnc  4096  ordsucss  4390  eqbrrdva  4679  elreldm  4735  elres  4825  xp11m  4947  ssrnres  4951  opelf  5264  dffo4  5536  dftpos3  6127  tfr1onlemaccex  6213  tfrcllemaccex  6226  nnaordex  6391  swoer  6425  map0g  6550  mapsn  6552  nneneq  6719  fnfi  6793  prarloclemlo  7270  genprndl  7297  genprndu  7298  cauappcvgprlemladdrl  7433  caucvgprlemladdrl  7454  caucvgsrlemoffres  7576  caucvgsr  7578  nntopi  7670  letr  7815  reapcotr  8328  apcotr  8337  mulext1  8342  cnstab  8375  lt2msq  8612  nneoor  9121  xrletr  9559  icoshft  9741  caucvgre  10721  absext  10803  rexico  10961  summodc  11120  gcdeq0  11592  tgcn  12304  cnptoprest  12335  metequiv2  12592  bj-nnsn  12872  bj-inf2vnlem2  13096
  Copyright terms: Public domain W3C validator