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

Theorem syl3an1 1232
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 1150 . 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 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:  syl3an1b  1235  syl3an1br  1238  wepo  4249  f1ofveu  5728  fovrnda  5880  smoiso  6165  tfrcl  6227  omv  6317  oeiv  6318  nndi  6348  nnmsucr  6350  f1oen2g  6615  f1dom2g  6616  undiffi  6779  prarloclemarch2  7191  distrnq0  7231  ltprordil  7361  1idprl  7362  1idpru  7363  ltpopr  7367  ltexprlemopu  7375  ltexprlemdisj  7378  ltexprlemfl  7381  ltexprlemfu  7383  ltexprlemru  7384  recexprlemdisj  7402  recexprlemss1l  7407  recexprlemss1u  7408  cnegexlem1  7901  msqge0  8341  mulge0  8344  divnegap  8426  divdiv32ap  8440  divneg2ap  8456  peano2uz  9327  lbzbi  9357  negqmod0  10044  modqmuladdnn0  10081  expnlbnd  10356  shftfvalg  10530  xrmaxaddlem  10969  retanclap  11328  tannegap  11334  demoivreALT  11378  gcd0id  11563  isprm3  11695  euclemma  11720  phiprmpw  11793  psmetcl  12390  xmetcl  12416  metcl  12417  meteq0  12424  metge0  12430  metsym  12435  blelrnps  12483  blelrn  12484  blssm  12485  blres  12498  mscl  12529  xmscl  12530  xmsge0  12531  xmseq0  12532  xmssym  12533  mopnin  12551
  Copyright terms: Public domain W3C validator