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

Theorem syl3an1 1203
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 1125 . 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 920
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 922
This theorem is referenced by:  syl3an1b  1206  syl3an1br  1209  wepo  4144  f1ofveu  5557  fovrnda  5701  smoiso  5977  tfrcl  6039  omv  6126  oeiv  6127  nndi  6157  nnmsucr  6159  f1oen2g  6330  f1dom2g  6331  undiffi  6476  prarloclemarch2  6757  distrnq0  6797  ltprordil  6927  1idprl  6928  1idpru  6929  ltpopr  6933  ltexprlemopu  6941  ltexprlemdisj  6944  ltexprlemfl  6947  ltexprlemfu  6949  ltexprlemru  6950  recexprlemdisj  6968  recexprlemss1l  6973  recexprlemss1u  6974  cnegexlem1  7436  msqge0  7869  mulge0  7872  divnegap  7947  divdiv32ap  7961  divneg2ap  7977  peano2uz  8838  lbzbi  8868  negqmod0  9499  modqmuladdnn0  9536  expnlbnd  9780  shftfvalg  9941  gcd0id  10611  isprm3  10741  euclemma  10766  phiprmpw  10839
  Copyright terms: Public domain W3C validator