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-mp 5  ax-1 6  ax-2 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  2909  opeldmg  4712  elreldm  4733  ssimaex  5448  resflem  5550  f1eqcocnv  5658  fliftfun  5663  isopolem  5689  isosolem  5691  brtposg  6117  issmo2  6152  nnmcl  6343  nnawordi  6377  nnmordi  6378  nnmord  6379  swoord1  6424  ecopovtrn  6492  ecopovtrng  6495  f1domg  6618  mapen  6706  mapxpen  6708  supmoti  6846  isotilem  6859  exmidomniim  6979  enq0tr  7206  prubl  7258  ltexprlemloc  7379  addextpr  7393  recexprlem1ssl  7405  recexprlem1ssu  7406  cauappcvgprlemdisj  7423  mulcmpblnr  7513  mulgt0sr  7550  map2psrprg  7577  ltleletr  7810  ltle  7815  ltadd2  8145  leltadd  8173  reapti  8304  apreap  8312  reapcotr  8323  apcotr  8332  addext  8335  mulext1  8337  cnstab  8370  zapne  9079  zextle  9096  prime  9104  uzin  9310  indstr  9340  supinfneg  9342  infsupneg  9343  ublbneg  9357  xrltle  9535  xrre2  9555  icc0r  9660  fzrevral  9836  flqge  10006  modqadd1  10085  modqmul1  10101  facdiv  10435  resqrexlemgt0  10743  abs00ap  10785  absext  10786  climshftlemg  11022  climcaucn  11071  dvds2lem  11412  dvdsfac  11465  ltoddhalfle  11497  ndvdsadd  11535  gcdaddm  11579  bezoutlembi  11600  gcdzeq  11617  algcvga  11639  rpdvds  11687  cncongr1  11691  cncongr2  11692  prmind2  11708  euclemma  11731  isprm6  11732  rpexp  11738  sqrt2irr  11747  fiinbas  12122  bastg  12136  tgcl  12139  opnssneib  12231  tgcnp  12284  iscnp4  12293  cnntr  12300  cnptopresti  12313  lmss  12321  lmtopcnp  12325  txdis  12352  xblss2ps  12479  xblss2  12480  blsscls2  12568  metequiv2  12571  bdxmet  12576  mulc1cncf  12651  cncfco  12653  triap  13058
  Copyright terms: Public domain W3C validator