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

Theorem sylanb 284
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanb.1  |-  ( ph  <->  ps )
sylanb.2  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylanb  |-  ( (
ph  /\  ch )  ->  th )

Proof of Theorem sylanb
StepHypRef Expression
1 sylanb.1 . . 3  |-  ( ph  <->  ps )
21biimpi 120 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 283 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> 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:  syl2anb  291  anabsan  575  2exeu  2118  eqtr2  2196  pm13.181  2429  rmob  3055  disjne  3476  seex  4334  tron  4381  fssres  5390  funbrfvb  5557  funopfvb  5558  fvelrnb  5562  fvco  5585  fvimacnvi  5629  ffvresb  5678  funresdfunsnss  5718  fvtp2g  5724  fvtp2  5727  fnex  5737  funex  5738  1st2nd  6179  dftpos4  6261  nnmsucr  6486  nnmcan  6517  xpmapenlem  6846  fundmfibi  6935  sup3exmid  8910  nzadd  9301  peano5uzti  9357  fnn0ind  9365  uztrn2  9541  irradd  9642  xltnegi  9831  xaddnemnf  9853  xaddnepnf  9854  xaddcom  9857  xnegdi  9864  elioore  9908  uzsubsubfz1  10043  fzo1fzo0n0  10178  elfzonelfzo  10225  qbtwnxr  10253  faclbnd  10714  faclbnd3  10716  dvdsprime  12114  pcgcd  12320  restuni  13543  stoig  13544  cnnei  13603  tgioo  13917  divcnap  13926  lgsdi  14309  bj-indind  14544
  Copyright terms: Public domain W3C validator