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  1723  eqreu  2798  onsucsssucr  4299  ordsucunielexmid  4320  ovi3  5738  tfrlem9  6038  dom2lem  6441  distrlem4prl  7087  distrlem4pru  7088  recexprlemm  7127  caucvgprlem1  7182  caucvgprprlemexb  7210  aptisr  7268  renegcl  7687  addid0  7795  remulext2  8018  mulext1  8030  apmul1  8194  nnge1  8380  0mnnnnn0  8638  nn0lt2  8761  zneo  8780  uzind2  8791  fzind  8794  nn0ind-raph  8796  ledivge1le  9135  elfzmlbp  9471  difelfznle  9474  elfzodifsumelfzo  9540  ssfzo12  9563  flqeqceilz  9653  addmodlteq  9733  uzsinds  9776  facdiv  10043  facwordi  10045  bcpasc  10071  addcn2  10593  mulcn2  10595  climrecvg1n  10629  odd2np1  10755  oddge22np1  10763  gcdaddm  10857  algcvgblem  10913  cncongr1  10967
  Copyright terms: Public domain W3C validator