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

Theorem syl3an1 1168
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 1090 . 2 ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))
3 syl3an1.2 . 2 ((𝜓𝜒𝜃) → 𝜏)
42, 3syl 14 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 885
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 887
This theorem is referenced by:  syl3an1b  1171  syl3an1br  1174  wepo  4096  f1ofveu  5500  fovrnda  5644  smoiso  5917  omv  6035  oeiv  6036  nndi  6065  nnmsucr  6067  f1oen2g  6235  f1dom2g  6236  prarloclemarch2  6515  distrnq0  6555  ltprordil  6685  1idprl  6686  1idpru  6687  ltpopr  6691  ltexprlemopu  6699  ltexprlemdisj  6702  ltexprlemfl  6705  ltexprlemfu  6707  ltexprlemru  6708  recexprlemdisj  6726  recexprlemss1l  6731  recexprlemss1u  6732  cnegexlem1  7184  msqge0  7605  mulge0  7608  divnegap  7681  divdiv32ap  7694  divneg2ap  7710  peano2uz  8524  lbzbi  8549  negqmod0  9171  expnlbnd  9371  shftfvalg  9417
  Copyright terms: Public domain W3C validator