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

Theorem syl3an2 1208
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 1142 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl5 32 . 2  |-  ( ps 
->  ( ph  ->  ( th  ->  ta ) ) )
543imp 1137 1  |-  ( ( ps  /\  ph  /\  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:  syl3an2b  1211  syl3an2br  1214  syl3anl2  1223  nndi  6239  nnmass  6240  prarloclemarch2  6968  1idprl  7139  1idpru  7140  recexprlem1ssl  7182  recexprlem1ssu  7183  msqge0  8083  mulge0  8086  divsubdirap  8165  divdiv32ap  8177  peano2uz  9061  fzoshftral  9637  expdivap  9994  ibcval5  10159  redivap  10296  imdivap  10303  absdiflt  10513  absdifle  10514  retanclap  11000  tannegap  11006  lcmgcdeq  11330  isprm3  11365  prmdvdsexpb  11393
  Copyright terms: Public domain W3C validator