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  3256  difprsnss  3532  trin2  4746  imadiflem  5009  fnun  5036  fco  5087  f1co  5132  foco  5147  f1oun  5177  f1oco  5180  eqfunfv  5302  ftpg  5379  issmo  5937  tfrlem5  5963  ener  6326  domtr  6332  unen  6361  xpdom2  6375  pm54.43  6518  axpre-lttrn  7112  axpre-mulgt0  7115  zmulcl  8485  qaddcl  8801  qmulcl  8803  rpaddcl  8838  rpmulcl  8839  rpdivcl  8840  xrltnsym  8944  xrlttri3  8948  ge0addcl  9080  ge0mulcl  9081  serige0  9570  expclzaplem  9597  expge0  9609  expge1  9610  qredeu  10623
  Copyright terms: Public domain W3C validator