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

Theorem syl3an 1158
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 1071 . 2 ((φ χ τ) → (ψ θ η))
5 syl3an.4 . 2 ((ψ θ η) → ζ)
64, 5syl 14 1 ((φ χ τ) → ζ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 867
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 869
This theorem is referenced by:  funtpg  4865  ftpg  5261  eloprabga  5503  addasspig  6177  mulasspig  6179  distrpig  6180  addcanpig  6181  mulcanpig  6182  ltapig  6185  distrnqg  6233  distrnq0  6301  cnegexlem2  6788  zletr  7866  zdivadd  7895
  Copyright terms: Public domain W3C validator