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

Theorem syl3an 1177
 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 1089 . 2 ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))
5 syl3an.4 . 2 ((𝜓𝜃𝜂) → 𝜁)
64, 5syl 14 1 ((𝜑𝜒𝜏) → 𝜁)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  funtpg  4950  ftpg  5347  eloprabga  5591  addasspig  6428  mulasspig  6430  distrpig  6431  addcanpig  6432  mulcanpig  6433  ltapig  6436  distrnqg  6485  distrnq0  6557  cnegexlem2  7187  zletr  8294  zdivadd  8329  iooneg  8856  fzen  8907  fzaddel  8922  fzrev  8946  fzrevral2  8968  fzshftral  8970  fzosubel2  9051  fzonn0p1p1  9069  resqrexlemover  9608
 Copyright terms: Public domain W3C validator