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

Theorem syl3an1 1207
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 1129 . 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 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  syl3an1b  1210  syl3an1br  1213  wepo  4186  f1ofveu  5640  fovrnda  5788  smoiso  6067  tfrcl  6129  omv  6216  oeiv  6217  nndi  6247  nnmsucr  6249  f1oen2g  6470  f1dom2g  6471  undiffi  6633  prarloclemarch2  6976  distrnq0  7016  ltprordil  7146  1idprl  7147  1idpru  7148  ltpopr  7152  ltexprlemopu  7160  ltexprlemdisj  7163  ltexprlemfl  7166  ltexprlemfu  7168  ltexprlemru  7169  recexprlemdisj  7187  recexprlemss1l  7192  recexprlemss1u  7193  cnegexlem1  7655  msqge0  8091  mulge0  8094  divnegap  8171  divdiv32ap  8185  divneg2ap  8201  peano2uz  9069  lbzbi  9099  negqmod0  9734  modqmuladdnn0  9771  expnlbnd  10074  shftfvalg  10248  retanclap  11009  tannegap  11015  demoivreALT  11059  gcd0id  11244  isprm3  11374  euclemma  11399  phiprmpw  11472
  Copyright terms: Public domain W3C validator