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

Theorem sylanb 278
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 118 . 2  |-  ( ph  ->  ps )
3 sylanb.2 . 2  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylan 277 1  |-  ( (
ph  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  syl2anb  285  anabsan  540  2exeu  2034  eqtr2  2100  pm13.181  2328  rmob  2907  disjne  3304  seex  4098  tron  4145  fssres  5097  funbrfvb  5248  funopfvb  5249  fvelrnb  5253  fvco  5275  fvimacnvi  5313  ffvresb  5360  fvtp2g  5402  fvtp2  5405  fnex  5415  funex  5416  1st2nd  5838  dftpos4  5912  nnmsucr  6132  nnmcan  6158  fundmfibi  6448  nzadd  8484  peano5uzti  8536  fnn0ind  8544  uztrn2  8717  irradd  8812  xltnegi  8978  elioore  9011  uzsubsubfz1  9143  fzo1fzo0n0  9269  elfzonelfzo  9316  qbtwnxr  9344  faclbnd  9765  faclbnd3  9767  dvdsprime  10648  bj-indind  10885
  Copyright terms: Public domain W3C validator