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

Theorem syl3an 1217
Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)
Hypotheses
Ref Expression
syl3an.1 (𝜑𝜓)
syl3an.2 (𝜒𝜃)
syl3an.3 (𝜏𝜂)
syl3an.4 ((𝜓𝜃𝜂) → 𝜁)
Assertion
Ref Expression
syl3an ((𝜑𝜒𝜏) → 𝜁)

Proof of Theorem syl3an
StepHypRef Expression
1 syl3an.1 . . 3 (𝜑𝜓)
2 syl3an.2 . . 3 (𝜒𝜃)
3 syl3an.3 . . 3 (𝜏𝜂)
41, 2, 33anim123i 1129 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 14 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 927
This theorem is referenced by:  syl2an3an  1235  funtpg  5080  ftpg  5497  eloprabga  5751  prfidisj  6693  addasspig  6952  mulasspig  6954  distrpig  6955  addcanpig  6956  mulcanpig  6957  ltapig  6960  distrnqg  7009  distrnq0  7081  cnegexlem2  7721  zletr  8862  zdivadd  8898  iooneg  9468  zltaddlt1le  9486  fzen  9520  fzaddel  9536  fzrev  9561  fzrevral2  9583  fzshftral  9585  fzosubel2  9669  fzonn0p1p1  9687  resqrexlemover  10506  fisum0diag2  10904  dvdsnegb  11154  muldvds1  11162  muldvds2  11163  dvdscmul  11164  dvdsmulc  11165  dvds2add  11171  dvds2sub  11172  dvdstr  11174  addmodlteqALT  11201  divalgb  11266  ndvdsadd  11272  absmulgcd  11347  rpmulgcd  11356  cncongr2  11427  hashdvds  11538
  Copyright terms: Public domain W3C validator