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

Theorem syl3an 1216
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 1128 . 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 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:  syl2an3an  1234  funtpg  5065  ftpg  5481  eloprabga  5735  prfidisj  6635  addasspig  6887  mulasspig  6889  distrpig  6890  addcanpig  6891  mulcanpig  6892  ltapig  6895  distrnqg  6944  distrnq0  7016  cnegexlem2  7656  zletr  8797  zdivadd  8833  iooneg  9403  zltaddlt1le  9421  fzen  9455  fzaddel  9470  fzrev  9494  fzrevral2  9516  fzshftral  9518  fzosubel2  9602  fzonn0p1p1  9620  resqrexlemover  10439  fisum0diag2  10837  dvdsnegb  11087  muldvds1  11095  muldvds2  11096  dvdscmul  11097  dvdsmulc  11098  dvds2add  11104  dvds2sub  11105  dvdstr  11107  addmodlteqALT  11134  divalgb  11199  ndvdsadd  11205  absmulgcd  11280  rpmulgcd  11289  cncongr2  11360  hashdvds  11471
  Copyright terms: Public domain W3C validator