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

Theorem syl3an2 1283
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 1204 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syl5 32 . 2  |-  ( ps 
->  ( ph  ->  ( th  ->  ta ) ) )
543imp 1195 1  |-  ( ( ps  /\  ph  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  syl3an2b  1286  syl3an2br  1289  syl3anl2  1298  nndi  6512  nnmass  6513  prarloclemarch2  7449  1idprl  7620  1idpru  7621  recexprlem1ssl  7663  recexprlem1ssu  7664  msqge0  8604  mulge0  8607  divsubdirap  8696  divdiv32ap  8708  peano2uz  9615  fzoshftral  10270  expdivap  10605  bcval5  10778  redivap  10918  imdivap  10925  absdiflt  11136  absdifle  11137  retanclap  11765  tannegap  11771  lcmgcdeq  12118  isprm3  12153  prmdvdsexpb  12184  dvdsprmpweqnn  12371  mulgaddcomlem  13102  mulginvcom  13104  cnpf2  14184  blres  14411
  Copyright terms: Public domain W3C validator