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  2911  opeldmg  4714  elreldm  4735  ssimaex  5450  resflem  5552  f1eqcocnv  5660  fliftfun  5665  isopolem  5691  isosolem  5693  brtposg  6119  issmo2  6154  nnmcl  6345  nnawordi  6379  nnmordi  6380  nnmord  6381  swoord1  6426  ecopovtrn  6494  ecopovtrng  6497  f1domg  6620  mapen  6708  mapxpen  6710  supmoti  6848  isotilem  6861  exmidomniim  6981  enq0tr  7210  prubl  7262  ltexprlemloc  7383  addextpr  7397  recexprlem1ssl  7409  recexprlem1ssu  7410  cauappcvgprlemdisj  7427  mulcmpblnr  7517  mulgt0sr  7554  map2psrprg  7581  ltleletr  7814  ltle  7819  ltadd2  8149  leltadd  8177  reapti  8309  apreap  8317  reapcotr  8328  apcotr  8337  addext  8340  mulext1  8342  cnstab  8375  zapne  9093  zextle  9110  prime  9118  uzin  9326  indstr  9356  supinfneg  9358  infsupneg  9359  ublbneg  9373  xrltle  9552  xrre2  9572  icc0r  9677  fzrevral  9853  flqge  10023  modqadd1  10102  modqmul1  10118  facdiv  10452  resqrexlemgt0  10760  abs00ap  10802  absext  10803  climshftlemg  11039  climcaucn  11088  dvds2lem  11432  dvdsfac  11485  ltoddhalfle  11517  ndvdsadd  11555  gcdaddm  11599  bezoutlembi  11620  gcdzeq  11637  algcvga  11659  rpdvds  11707  cncongr1  11711  cncongr2  11712  prmind2  11728  euclemma  11751  isprm6  11752  rpexp  11758  sqrt2irr  11767  fiinbas  12143  bastg  12157  tgcl  12160  opnssneib  12252  tgcnp  12305  iscnp4  12314  cnntr  12321  cnptopresti  12334  lmss  12342  lmtopcnp  12346  txdis  12373  xblss2ps  12500  xblss2  12501  blsscls2  12589  metequiv2  12592  bdxmet  12597  mulc1cncf  12672  cncfco  12674  sincosq2sgn  12835  sincosq3sgn  12836  sincosq4sgn  12837  triap  13151
  Copyright terms: Public domain W3C validator