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

Theorem syl2anb 289
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 282 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2b 285 1  |-  ( (
ph  /\  ta )  ->  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:  sylancb  415  stdcndc  831  reupick3  3392  difprsnss  3695  trin2  4978  imadiflem  5250  fnun  5277  fco  5336  f1co  5388  foco  5403  f1oun  5435  f1oco  5438  eqfunfv  5571  ftpg  5652  issmo  6236  tfrlem5  6262  ener  6725  domtr  6731  unen  6762  xpdom2  6777  mapen  6792  pm54.43  7126  axpre-lttrn  7805  axpre-mulgt0  7808  zmulcl  9221  qaddcl  9545  qmulcl  9547  rpaddcl  9585  rpmulcl  9586  rpdivcl  9587  xrltnsym  9701  xrlttri3  9705  ge0addcl  9886  ge0mulcl  9887  ge0xaddcl  9888  expclzaplem  10447  expge0  10459  expge1  10460  hashfacen  10711  qredeu  11978  nn0gcdsq  12079  cnovex  12638  iscn2  12642  txuni  12705  txcn  12717
  Copyright terms: Public domain W3C validator