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

Theorem syl3c 63
Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)
Hypotheses
Ref Expression
syl3c.1  |-  ( ph  ->  ps )
syl3c.2  |-  ( ph  ->  ch )
syl3c.3  |-  ( ph  ->  th )
syl3c.4  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
Assertion
Ref Expression
syl3c  |-  ( ph  ->  ta )

Proof of Theorem syl3c
StepHypRef Expression
1 syl3c.3 . 2  |-  ( ph  ->  th )
2 syl3c.1 . . 3  |-  ( ph  ->  ps )
3 syl3c.2 . . 3  |-  ( ph  ->  ch )
4 syl3c.4 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
52, 3, 4sylc 62 . 2  |-  ( ph  ->  ( th  ->  ta ) )
61, 5mpd 13 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  bilukdc  1374  disjiun  3924  tfrlem1  6205  tfrcl  6261  mkvprop  7032  ccfunen  7079  caucvgprprlemval  7503  suplocsrlem  7623  peano5uzti  9166  zfz1iso  10591  lcmneg  11761  prmind2  11807  cnmpt12  12465  cnmpt22  12472  limccnp2lem  12823  sbthom  13274
  Copyright terms: Public domain W3C validator