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

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

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylibrd.2 . . 3  |-  ( ph  ->  ( th  <->  ch )
)
32biimprd 151 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 44 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  3imtr4d  196  sbciegft  2816  opeldmg  4568  elreldm  4588  ssimaex  5262  f1eqcocnv  5459  fliftfun  5464  isopolem  5489  isosolem  5491  brtposg  5900  issmo2  5935  rdgon  6004  frecsuclem3  6021  freccl  6024  nnmcl  6091  nnawordi  6119  nnmordi  6120  nnmord  6121  swoord1  6166  ecopovtrn  6234  ecopovtrng  6237  f1domg  6269  supmoti  6399  isotilem  6410  enq0tr  6590  prubl  6642  ltexprlemloc  6763  addextpr  6777  recexprlem1ssl  6789  recexprlem1ssu  6790  cauappcvgprlemdisj  6807  mulcmpblnr  6884  mulgt0sr  6920  ltleletr  7159  ltle  7164  ltadd2  7488  leltadd  7516  reapti  7644  apreap  7652  reapcotr  7663  apcotr  7672  addext  7675  mulext1  7677  zapne  8373  zextle  8389  prime  8396  uzin  8601  indstr  8632  ublbneg  8645  xrltle  8820  xrre2  8835  icc0r  8896  fzrevral  9069  flqge  9232  modqadd1  9311  modqmul1  9327  facdiv  9606  resqrexlemgt0  9847  abs00ap  9889  absext  9890  climshftlemg  10054  climcaucn  10101  dvds2lem  10120  dvdsfac  10172  ltoddhalfle  10205  ndvdsadd  10243  sqrt2irr  10251  ialgcvga  10273
  Copyright terms: Public domain W3C validator