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

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

Proof of Theorem syl3an2
StepHypRef Expression
1 syl3an2.1 . . 3  |-  ( ph  ->  ch )
2 syl3an2.2 . . . 4  |-  ( ( ps  /\  ch  /\  th )  ->  ta )
323exp 1163 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl5 32 . 2  |-  ( ps 
->  ( ph  ->  ( th  ->  ta ) ) )
543imp 1158 1  |-  ( ( ps  /\  ph  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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:  syl3an2b  1236  syl3an2br  1239  syl3anl2  1248  nndi  6336  nnmass  6337  prarloclemarch2  7175  1idprl  7346  1idpru  7347  recexprlem1ssl  7389  recexprlem1ssu  7390  msqge0  8296  mulge0  8299  divsubdirap  8381  divdiv32ap  8393  peano2uz  9280  fzoshftral  9908  expdivap  10237  bcval5  10402  redivap  10539  imdivap  10546  absdiflt  10756  absdifle  10757  retanclap  11280  tannegap  11286  lcmgcdeq  11610  isprm3  11645  prmdvdsexpb  11673  cnpf2  12218  blres  12423
  Copyright terms: Public domain W3C validator