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  364  con2biddc  870  nfalt  1565  alexim  1632  19.36-1  1660  ax11ev  1815  equs5or  1817  necon2bd  2392  necon2d  2393  necon1bbiddc  2397  necon2abiddc  2400  necon2bbiddc  2401  necon4idc  2403  necon4ddc  2406  necon1bddc  2411  spc2gv  2815  spc3gv  2817  mo2icl  2903  reupick  3404  prneimg  3751  invdisj  3973  trin  4087  exmidsssnc  4179  ordsucss  4478  eqbrrdva  4771  elreldm  4827  elres  4917  xp11m  5039  ssrnres  5043  opelf  5356  dffo4  5630  dftpos3  6224  tfr1onlemaccex  6310  tfrcllemaccex  6323  nnaordex  6489  swoer  6523  map0g  6648  mapsn  6650  nneneq  6817  fnfi  6896  prarloclemlo  7429  genprndl  7456  genprndu  7457  cauappcvgprlemladdrl  7592  caucvgprlemladdrl  7613  caucvgsrlemoffres  7735  caucvgsr  7737  nntopi  7829  letr  7975  reapcotr  8490  apcotr  8499  mulext1  8504  lt2msq  8775  nneoor  9287  xrletr  9738  icoshft  9920  caucvgre  10917  absext  10999  rexico  11157  summodc  11318  gcdeq0  11904  tgcn  12806  cnptoprest  12837  metequiv2  13094  bj-nnsn  13508  bj-inf2vnlem2  13746
  Copyright terms: Public domain W3C validator