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

Theorem syl3an2 1180
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 1114 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl5 32 . 2  |-  ( ps 
->  ( ph  ->  ( th  ->  ta ) ) )
543imp 1109 1  |-  ( ( ps  /\  ph  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  syl3an2b  1183  syl3an2br  1186  syl3anl2  1195  nndi  6096  nnmass  6097  prarloclemarch2  6575  1idprl  6746  1idpru  6747  recexprlem1ssl  6789  recexprlem1ssu  6790  msqge0  7681  mulge0  7684  divsubdirap  7759  divdiv32ap  7771  peano2uz  8622  fzoshftral  9196  expdivap  9471  ibcval5  9631  redivap  9702  imdivap  9709  absdiflt  9919  absdifle  9920
  Copyright terms: Public domain W3C validator