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

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

Proof of Theorem syl3an1
StepHypRef Expression
1 syl3an1.1 . . 3 (𝜑𝜓)
213anim1i 1125 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 14 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  syl3an1b  1206  syl3an1br  1209  wepo  4122  f1ofveu  5531  fovrnda  5675  smoiso  5951  tfrcl  6013  omv  6099  oeiv  6100  nndi  6130  nnmsucr  6132  f1oen2g  6302  f1dom2g  6303  prarloclemarch2  6671  distrnq0  6711  ltprordil  6841  1idprl  6842  1idpru  6843  ltpopr  6847  ltexprlemopu  6855  ltexprlemdisj  6858  ltexprlemfl  6861  ltexprlemfu  6863  ltexprlemru  6864  recexprlemdisj  6882  recexprlemss1l  6887  recexprlemss1u  6888  cnegexlem1  7350  msqge0  7783  mulge0  7786  divnegap  7861  divdiv32ap  7875  divneg2ap  7891  peano2uz  8752  lbzbi  8782  negqmod0  9413  modqmuladdnn0  9450  expnlbnd  9694  shftfvalg  9844  gcd0id  10514  isprm3  10644  euclemma  10669
  Copyright terms: Public domain W3C validator