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

Theorem syl6an 1414
Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)
Hypotheses
Ref Expression
syl6an.1  |-  ( ph  ->  ps )
syl6an.2  |-  ( ph  ->  ( ch  ->  th )
)
syl6an.3  |-  ( ( ps  /\  th )  ->  ta )
Assertion
Ref Expression
syl6an  |-  ( ph  ->  ( ch  ->  ta ) )

Proof of Theorem syl6an
StepHypRef Expression
1 syl6an.2 . . 3  |-  ( ph  ->  ( ch  ->  th )
)
2 syl6an.1 . . 3  |-  ( ph  ->  ps )
31, 2jctild 314 . 2  |-  ( ph  ->  ( ch  ->  ( ps  /\  th ) ) )
4 syl6an.3 . 2  |-  ( ( ps  /\  th )  ->  ta )
53, 4syl6 33 1  |-  ( ph  ->  ( ch  ->  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-ia3 107
This theorem is referenced by:  mapxpen  6793  prarloclem5  7420  ltsopr  7516  suplocsrlem  7728  nominpos  9070  ublbneg  9522  absle  10989  rexanre  11120  rexico  11121  climshftlemg  11199  serf0  11249  dvds1lem  11698  dvds2lem  11699  lmconst  12627  addcncntoplem  12962  bj-indind  13518
  Copyright terms: Public domain W3C validator