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

Theorem syl3an3 1251
 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 1180 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl7 69 . 2 (𝜓 → (𝜒 → (𝜑𝜏)))
543imp 1175 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:  syl3an3b  1254  syl3an3br  1257  vtoclgft  2736  ovmpox  5899  ovmpoga  5900  nnanq0  7273  apreim  8372  apsub1  8411  divassap  8457  ltmul2  8621  xleadd1  9665  xltadd2  9667  elfzo  9933  fzodcel  9936  subcn2  11087  mulcn2  11088  ndvdsp1  11636  gcddiv  11714  lcmneg  11762  neipsm  12333  opnneip  12338  hmeof1o2  12487  blcntrps  12594  blcntr  12595  neibl  12670  blnei  12671  metss  12673
 Copyright terms: Public domain W3C validator