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

Theorem syl3an1 1234
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 1152 . 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 947
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 949
This theorem is referenced by:  syl3an1b  1237  syl3an1br  1240  wepo  4251  f1ofveu  5730  fovrnda  5882  smoiso  6167  tfrcl  6229  omv  6319  oeiv  6320  nndi  6350  nnmsucr  6352  f1oen2g  6617  f1dom2g  6618  undiffi  6781  prarloclemarch2  7195  distrnq0  7235  ltprordil  7365  1idprl  7366  1idpru  7367  ltpopr  7371  ltexprlemopu  7379  ltexprlemdisj  7382  ltexprlemfl  7385  ltexprlemfu  7387  ltexprlemru  7388  recexprlemdisj  7406  recexprlemss1l  7411  recexprlemss1u  7412  cnegexlem1  7905  msqge0  8346  mulge0  8349  divnegap  8434  divdiv32ap  8448  divneg2ap  8464  peano2uz  9346  lbzbi  9376  negqmod0  10072  modqmuladdnn0  10109  expnlbnd  10384  shftfvalg  10558  xrmaxaddlem  10997  retanclap  11356  tannegap  11362  demoivreALT  11407  gcd0id  11594  isprm3  11726  euclemma  11751  phiprmpw  11825  psmetcl  12422  xmetcl  12448  metcl  12449  meteq0  12456  metge0  12462  metsym  12467  blelrnps  12515  blelrn  12516  blssm  12517  blres  12530  mscl  12561  xmscl  12562  xmsge0  12563  xmseq0  12564  xmssym  12565  mopnin  12583  sincosq1sgn  12834  sincosq2sgn  12835  sincosq3sgn  12836  sincosq4sgn  12837
  Copyright terms: Public domain W3C validator