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

Theorem sylibrd 168
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 157 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3syld 45 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr4d  202  sbciegft  2870  opeldmg  4654  elreldm  4674  ssimaex  5378  resflem  5476  f1eqcocnv  5584  fliftfun  5589  isopolem  5615  isosolem  5617  brtposg  6033  issmo2  6068  nnmcl  6256  nnawordi  6288  nnmordi  6289  nnmord  6290  swoord1  6335  ecopovtrn  6403  ecopovtrng  6406  f1domg  6529  mapen  6616  mapxpen  6618  supmoti  6742  isotilem  6755  exmidomniim  6858  enq0tr  7054  prubl  7106  ltexprlemloc  7227  addextpr  7241  recexprlem1ssl  7253  recexprlem1ssu  7254  cauappcvgprlemdisj  7271  mulcmpblnr  7348  mulgt0sr  7384  ltleletr  7628  ltle  7633  ltadd2  7958  leltadd  7986  reapti  8117  apreap  8125  reapcotr  8136  apcotr  8145  addext  8148  mulext1  8150  zapne  8882  zextle  8898  prime  8906  uzin  9112  indstr  9142  supinfneg  9144  infsupneg  9145  ublbneg  9159  xrltle  9329  xrre2  9344  icc0r  9405  fzrevral  9580  flqge  9750  modqadd1  9829  modqmul1  9845  facdiv  10207  resqrexlemgt0  10514  abs00ap  10556  absext  10557  climshftlemg  10751  climcaucn  10801  dvds2lem  11147  dvdsfac  11200  ltoddhalfle  11232  ndvdsadd  11270  gcdaddm  11314  bezoutlembi  11333  gcdzeq  11350  algcvga  11372  rpdvds  11420  cncongr1  11424  cncongr2  11425  prmind2  11441  euclemma  11464  isprm6  11465  rpexp  11471  sqrt2irr  11480  fiinbas  11808  bastg  11822  tgcl  11825  mulc1cncf  11918  cncfco  11920
  Copyright terms: Public domain W3C validator