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

Theorem sylan9 407
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypotheses
Ref Expression
sylan9.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylan9.2  |-  ( th 
->  ( ch  ->  ta ) )
Assertion
Ref Expression
sylan9  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )

Proof of Theorem sylan9
StepHypRef Expression
1 sylan9.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylan9.2 . . 3  |-  ( th 
->  ( ch  ->  ta ) )
31, 2syl9 72 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ta ) ) )
43imp 123 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106
This theorem is referenced by:  sbequi  1812  rspc2  2804  rspc3v  2809  copsexg  4174  chfnrn  5539  ffnfv  5586  f1elima  5682  smoel2  6208  th3q  6542  fiintim  6825  addnnnq0  7281  mulnnnq0  7282  addsrpr  7577  mulsrpr  7578  cau3lem  10918  rescncf  12776
  Copyright terms: Public domain W3C validator