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  1385  disjiun  3972  tfrlem1  6268  tfrcl  6324  mkvprop  7114  ccfunen  7197  caucvgprprlemval  7621  suplocsrlem  7741  peano5uzti  9291  zfz1iso  10744  lcmneg  11995  prmind2  12041  pcfac  12269  cnmpt12  12854  cnmpt22  12861  limccnp2lem  13212  sbthom  13766
  Copyright terms: Public domain W3C validator