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

Theorem syl3an3 1210
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an3.1 (𝜑𝜃)
syl3an3.2 ((𝜓𝜒𝜃) → 𝜏)
Assertion
Ref Expression
syl3an3 ((𝜓𝜒𝜑) → 𝜏)

Proof of Theorem syl3an3
StepHypRef Expression
1 syl3an3.1 . . 3 (𝜑𝜃)
2 syl3an3.2 . . . 4 ((𝜓𝜒𝜃) → 𝜏)
323exp 1143 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl7 69 . 2 (𝜓 → (𝜒 → (𝜑𝜏)))
543imp 1138 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:  syl3an3b  1213  syl3an3br  1216  vtoclgft  2670  ovmpt2x  5787  ovmpt2ga  5788  nnanq0  7078  apreim  8141  apsub1  8178  divassap  8218  ltmul2  8378  elfzo  9621  fzodcel  9624  subcn2  10761  mulcn2  10762  ndvdsp1  11271  gcddiv  11347  lcmneg  11395
  Copyright terms: Public domain W3C validator