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

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

Proof of Theorem syl3an1
StepHypRef Expression
1 syl3an1.1 . . 3  |-  ( ph  ->  ps )
213anim1i 1101 . 2  |-  ( (
ph  /\  ch  /\  th )  ->  ( ps  /\  ch  /\  th ) )
3 syl3an1.2 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
42, 3syl 14 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  syl3an1b  1182  syl3an1br  1185  wepo  4123  f1ofveu  5527  fovrnda  5671  smoiso  5947  omv  6065  oeiv  6066  nndi  6095  nnmsucr  6097  f1oen2g  6265  f1dom2g  6266  prarloclemarch2  6574  distrnq0  6614  ltprordil  6744  1idprl  6745  1idpru  6746  ltpopr  6750  ltexprlemopu  6758  ltexprlemdisj  6761  ltexprlemfl  6764  ltexprlemfu  6766  ltexprlemru  6767  recexprlemdisj  6785  recexprlemss1l  6790  recexprlemss1u  6791  cnegexlem1  7248  msqge0  7680  mulge0  7683  divnegap  7756  divdiv32ap  7770  divneg2ap  7786  peano2uz  8621  lbzbi  8647  negqmod0  9275  modqmuladdnn0  9312  expnlbnd  9534  shftfvalg  9640
  Copyright terms: Public domain W3C validator