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

Theorem syl3an1 1249
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 1167 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 14 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:  syl3an1b  1252  syl3an1br  1255  wepo  4281  f1ofveu  5762  fovrnda  5914  smoiso  6199  tfrcl  6261  omv  6351  oeiv  6352  nndi  6382  nnmsucr  6384  f1oen2g  6649  f1dom2g  6650  undiffi  6813  prarloclemarch2  7239  distrnq0  7279  ltprordil  7409  1idprl  7410  1idpru  7411  ltpopr  7415  ltexprlemopu  7423  ltexprlemdisj  7426  ltexprlemfl  7429  ltexprlemfu  7431  ltexprlemru  7432  recexprlemdisj  7450  recexprlemss1l  7455  recexprlemss1u  7456  cnegexlem1  7949  msqge0  8390  mulge0  8393  divnegap  8478  divdiv32ap  8492  divneg2ap  8508  peano2uz  9390  lbzbi  9420  negqmod0  10116  modqmuladdnn0  10153  expnlbnd  10428  shftfvalg  10602  xrmaxaddlem  11041  retanclap  11440  tannegap  11446  demoivreALT  11491  gcd0id  11678  isprm3  11810  euclemma  11835  phiprmpw  11909  psmetcl  12509  xmetcl  12535  metcl  12536  meteq0  12543  metge0  12549  metsym  12554  blelrnps  12602  blelrn  12603  blssm  12604  blres  12617  mscl  12648  xmscl  12649  xmsge0  12650  xmseq0  12651  xmssym  12652  mopnin  12670  sincosq1sgn  12929  sincosq2sgn  12930  sincosq3sgn  12931  sincosq4sgn  12932
  Copyright terms: Public domain W3C validator