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

Theorem sylbird 170
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 158 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 sylbird.2 . 2  |-  ( ph  ->  ( ch  ->  th )
)
42, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  3imtr3d  202  drex1  1798  eqreu  2929  onsucsssucr  4504  ordsucunielexmid  4526  ovi3  6004  tfrlem9  6313  dom2lem  6765  distrlem4prl  7561  distrlem4pru  7562  recexprlemm  7601  caucvgprlem1  7656  caucvgprprlemexb  7684  aptisr  7756  map2psrprg  7782  renegcl  8195  addid0  8307  remulext2  8534  mulext1  8546  apmul1  8721  nnge1  8918  0mnnnnn0  9184  nn0lt2  9310  zneo  9330  uzind2  9341  fzind  9344  nn0ind-raph  9346  ledivge1le  9700  elfzmlbp  10105  difelfznle  10108  elfzodifsumelfzo  10174  ssfzo12  10197  flqeqceilz  10291  addmodlteq  10371  uzsinds  10415  qsqeqor  10603  facdiv  10689  facwordi  10691  bcpasc  10717  addcn2  11289  mulcn2  11291  climrecvg1n  11327  odd2np1  11848  oddge22np1  11856  gcdaddm  11955  algcvgblem  12019  cncongr1  12073  pcdvdsb  12289  pcaddlem  12308  infpnlem1  12327  prmunb  12330  metss2lem  13630  2sqlem6  14089
  Copyright terms: Public domain W3C validator