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

Theorem sylbird 168
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbird.1  |-  ( ph  ->  ( ch  <->  ps )
)
sylbird.2  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
sylbird  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylbird
StepHypRef Expression
1 sylbird.1 . . 3  |-  ( ph  ->  ( ch  <->  ps )
)
21biimprd 156 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 44 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:  3imtr3d  200  drex1  1721  eqreu  2793  onsucsssucr  4281  ordsucunielexmid  4302  ovi3  5689  tfrlem9  5989  dom2lem  6341  distrlem4prl  6906  distrlem4pru  6907  recexprlemm  6946  caucvgprlem1  7001  caucvgprprlemexb  7029  aptisr  7087  renegcl  7506  addid0  7614  remulext2  7837  mulext1  7849  apmul1  8013  nnge1  8199  0mnnnnn0  8457  nn0lt2  8580  zneo  8599  uzind2  8610  fzind  8613  nn0ind-raph  8615  ledivge1le  8954  elfzmlbp  9290  difelfznle  9293  elfzodifsumelfzo  9357  ssfzo12  9380  flqeqceilz  9470  addmodlteq  9550  uzsinds  9588  facdiv  9832  facwordi  9834  bcpasc  9860  addcn2  10368  mulcn2  10370  climrecvg1n  10404  odd2np1  10498  oddge22np1  10506  gcdaddm  10600  algcvgblem  10656  cncongr1  10710
  Copyright terms: Public domain W3C validator