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  6517  distrnq0  6557  ltprordil  6687  1idprl  6688  1idpru  6689  ltpopr  6693  ltexprlemopu  6701  ltexprlemdisj  6704  ltexprlemfl  6707  ltexprlemfu  6709  ltexprlemru  6710  recexprlemdisj  6728  recexprlemss1l  6733  recexprlemss1u  6734  cnegexlem1  7186  msqge0  7607  mulge0  7610  divnegap  7683  divdiv32ap  7696  divneg2ap  7712  peano2uz  8526  lbzbi  8551  negqmod0  9173  expnlbnd  9373  shftfvalg  9419
 Copyright terms: Public domain W3C validator