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

Theorem sylanb 282
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 119 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 281 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> 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:  syl2anb  289  anabsan  565  2exeu  2092  eqtr2  2159  pm13.181  2391  rmob  3004  disjne  3420  seex  4264  tron  4311  fssres  5305  funbrfvb  5471  funopfvb  5472  fvelrnb  5476  fvco  5498  fvimacnvi  5541  ffvresb  5590  funresdfunsnss  5630  fvtp2g  5636  fvtp2  5639  fnex  5649  funex  5650  1st2nd  6086  dftpos4  6167  nnmsucr  6391  nnmcan  6422  xpmapenlem  6750  fundmfibi  6834  sup3exmid  8738  nzadd  9129  peano5uzti  9182  fnn0ind  9190  uztrn2  9366  irradd  9464  xltnegi  9647  xaddnemnf  9669  xaddnepnf  9670  xaddcom  9673  xnegdi  9680  elioore  9724  uzsubsubfz1  9858  fzo1fzo0n0  9990  elfzonelfzo  10037  qbtwnxr  10065  faclbnd  10518  faclbnd3  10520  dvdsprime  11837  restuni  12378  stoig  12379  cnnei  12438  tgioo  12752  divcnap  12761  bj-indind  13299
  Copyright terms: Public domain W3C validator