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

Theorem syl3an 1188
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 1100 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 14 1 ((𝜑𝜒𝜏) → 𝜁)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  funtpg  4978  ftpg  5375  eloprabga  5619  addasspig  6486  mulasspig  6488  distrpig  6489  addcanpig  6490  mulcanpig  6491  ltapig  6494  distrnqg  6543  distrnq0  6615  cnegexlem2  7250  zletr  8351  zdivadd  8387  iooneg  8957  zltaddlt1le  8975  fzen  9009  fzaddel  9024  fzrev  9048  fzrevral2  9070  fzshftral  9072  fzosubel2  9153  fzonn0p1p1  9171  resqrexlemover  9837  dvdsnegb  10125  muldvds1  10132  muldvds2  10133  dvdscmul  10134  dvdsmulc  10135  dvds2add  10141  dvds2sub  10142  dvdstr  10144  addmodlteqALT  10171  divalgb  10237  ndvdsadd  10243
  Copyright terms: Public domain W3C validator