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

Theorem syl3an 1258
 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 1166 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 14 1 ((𝜑𝜒𝜏) → 𝜁)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 962 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 964 This theorem is referenced by:  syl2an3an  1276  funtpg  5174  ftpg  5604  eloprabga  5858  prfidisj  6815  djuenun  7068  addasspig  7145  mulasspig  7147  distrpig  7148  addcanpig  7149  mulcanpig  7150  ltapig  7153  distrnqg  7202  distrnq0  7274  cnegexlem2  7945  zletr  9110  zdivadd  9147  xaddass  9659  iooneg  9778  zltaddlt1le  9796  fzen  9830  fzaddel  9846  fzrev  9871  fzrevral2  9893  fzshftral  9895  fzosubel2  9979  fzonn0p1p1  9997  resqrexlemover  10789  fisum0diag2  11223  dvdsnegb  11517  muldvds1  11525  muldvds2  11526  dvdscmul  11527  dvdsmulc  11528  dvds2add  11534  dvds2sub  11535  dvdstr  11537  addmodlteqALT  11564  divalgb  11629  ndvdsadd  11635  absmulgcd  11712  rpmulgcd  11721  cncongr2  11792  hashdvds  11904
 Copyright terms: Public domain W3C validator