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

Theorem syl3an 1212
Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)
Hypotheses
Ref Expression
syl3an.1  |-  ( ph  ->  ps )
syl3an.2  |-  ( ch 
->  th )
syl3an.3  |-  ( ta 
->  et )
syl3an.4  |-  ( ( ps  /\  th  /\  et )  ->  ze )
Assertion
Ref Expression
syl3an  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )

Proof of Theorem syl3an
StepHypRef Expression
1 syl3an.1 . . 3  |-  ( ph  ->  ps )
2 syl3an.2 . . 3  |-  ( ch 
->  th )
3 syl3an.3 . . 3  |-  ( ta 
->  et )
41, 2, 33anim123i 1124 . 2  |-  ( (
ph  /\  ch  /\  ta )  ->  ( ps  /\  th 
/\  et ) )
5 syl3an.4 . 2  |-  ( ( ps  /\  th  /\  et )  ->  ze )
64, 5syl 14 1  |-  ( (
ph  /\  ch  /\  ta )  ->  ze )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 920
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 922
This theorem is referenced by:  syl2an3an  1230  funtpg  4981  ftpg  5379  eloprabga  5622  addasspig  6582  mulasspig  6584  distrpig  6585  addcanpig  6586  mulcanpig  6587  ltapig  6590  distrnqg  6639  distrnq0  6711  cnegexlem2  7351  zletr  8481  zdivadd  8517  iooneg  9086  zltaddlt1le  9104  fzen  9138  fzaddel  9153  fzrev  9177  fzrevral2  9199  fzshftral  9201  fzosubel2  9281  fzonn0p1p1  9299  resqrexlemover  10034  dvdsnegb  10357  muldvds1  10365  muldvds2  10366  dvdscmul  10367  dvdsmulc  10368  dvds2add  10374  dvds2sub  10375  dvdstr  10377  addmodlteqALT  10404  divalgb  10469  ndvdsadd  10475  absmulgcd  10550  rpmulgcd  10559  cncongr2  10630
  Copyright terms: Public domain W3C validator