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

Theorem syl3an3 1234
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1  |-  ( ph  ->  th )
syl3an3.2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
Assertion
Ref Expression
syl3an3  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3  |-  ( ph  ->  th )
2 syl3an3.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1163 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl7 69 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  ta ) ) )
543imp 1158 1  |-  ( ( ps  /\  ch  /\  ph )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  syl3an3b  1237  syl3an3br  1240  vtoclgft  2708  ovmpox  5865  ovmpoga  5866  nnanq0  7230  apreim  8328  apsub1  8366  divassap  8410  ltmul2  8571  xleadd1  9598  xltadd2  9600  elfzo  9866  fzodcel  9869  subcn2  11020  mulcn2  11021  ndvdsp1  11525  gcddiv  11603  lcmneg  11651  neipsm  12218  opnneip  12223  hmeof1o2  12372  blcntrps  12479  blcntr  12480  neibl  12555  blnei  12556  metss  12558
  Copyright terms: Public domain W3C validator