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

Theorem syl2anb 285
Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1  |-  ( ph  <->  ps )
syl2anb.2  |-  ( ta  <->  ch )
syl2anb.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anb  |-  ( (
ph  /\  ta )  ->  th )

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2  |-  ( ta  <->  ch )
2 syl2anb.1 . . 3  |-  ( ph  <->  ps )
3 syl2anb.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
42, 3sylanb 278 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2b 281 1  |-  ( (
ph  /\  ta )  ->  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:  sylancb  409  reupick3  3282  difprsnss  3570  trin2  4810  imadiflem  5079  fnun  5106  fco  5161  f1co  5212  foco  5227  f1oun  5257  f1oco  5260  eqfunfv  5386  ftpg  5465  issmo  6035  tfrlem5  6061  ener  6476  domtr  6482  unen  6513  xpdom2  6527  mapen  6542  pm54.43  6797  axpre-lttrn  7398  axpre-mulgt0  7401  zmulcl  8773  qaddcl  9089  qmulcl  9091  rpaddcl  9126  rpmulcl  9127  rpdivcl  9128  xrltnsym  9232  xrlttri3  9236  ge0addcl  9368  ge0mulcl  9369  expclzaplem  9944  expge0  9956  expge1  9957  hashfacen  10206  qredeu  11172  nn0gcdsq  11271
  Copyright terms: Public domain W3C validator