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

Theorem syl2anb 291
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 284 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4sylan2b 287 1  |-  ( (
ph  /\  ta )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  sylancb  418  stdcndc  845  reupick3  3420  difprsnss  3730  trin2  5020  imadiflem  5295  fnun  5322  fco  5381  f1co  5433  foco  5448  f1oun  5481  f1oco  5484  eqfunfv  5618  ftpg  5700  issmo  6288  tfrlem5  6314  ener  6778  domtr  6784  unen  6815  xpdom2  6830  mapen  6845  pm54.43  7188  axpre-lttrn  7882  axpre-mulgt0  7885  zmulcl  9304  qaddcl  9633  qmulcl  9635  rpaddcl  9675  rpmulcl  9676  rpdivcl  9677  xrltnsym  9791  xrlttri3  9795  ge0addcl  9979  ge0mulcl  9980  ge0xaddcl  9981  expclzaplem  10541  expge0  10553  expge1  10554  hashfacen  10811  qredeu  12091  nn0gcdsq  12194  mul4sq  12386  cnovex  13627  iscn2  13631  txuni  13694  txcn  13706  lgsne0  14370  mul2sq  14383
  Copyright terms: Public domain W3C validator