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

Theorem sylan9 409
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 124 1  |-  ( (
ph  /\  th )  ->  ( ps  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem is referenced by:  sbequi  1839  rspc2  2852  rspc3v  2857  copsexg  4240  chfnrn  5622  ffnfv  5669  f1elima  5767  smoel2  6297  th3q  6633  fiintim  6921  addnnnq0  7426  mulnnnq0  7427  addsrpr  7722  mulsrpr  7723  cau3lem  11094  rescncf  13701
  Copyright terms: Public domain W3C validator