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

Theorem syl3an 1241
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 1149 . 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 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  syl2an3an  1259  funtpg  5142  ftpg  5570  eloprabga  5824  prfidisj  6781  djuenun  7032  addasspig  7102  mulasspig  7104  distrpig  7105  addcanpig  7106  mulcanpig  7107  ltapig  7110  distrnqg  7159  distrnq0  7231  cnegexlem2  7902  zletr  9057  zdivadd  9094  xaddass  9603  iooneg  9722  zltaddlt1le  9740  fzen  9774  fzaddel  9790  fzrev  9815  fzrevral2  9837  fzshftral  9839  fzosubel2  9923  fzonn0p1p1  9941  resqrexlemover  10733  fisum0diag2  11167  dvdsnegb  11417  muldvds1  11425  muldvds2  11426  dvdscmul  11427  dvdsmulc  11428  dvds2add  11434  dvds2sub  11435  dvdstr  11437  addmodlteqALT  11464  divalgb  11529  ndvdsadd  11535  absmulgcd  11612  rpmulgcd  11621  cncongr2  11692  hashdvds  11803
  Copyright terms: Public domain W3C validator