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

Theorem syl3an1 1167
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 1089 . 2 ((φ χ θ) → (ψ χ θ))
3 syl3an1.2 . 2 ((ψ χ θ) → τ)
42, 3syl 14 1 ((φ χ θ) → τ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
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 886
This theorem is referenced by:  syl3an1b  1170  syl3an1br  1173  f1ofveu  5443  fovrnda  5586  smoiso  5858  omv  5974  oeiv  5975  nndi  6004  nnmsucr  6006  f1oen2g  6171  f1dom2g  6172  prarloclemarch2  6402  distrnq0  6441  ltprordil  6564  1idprl  6565  1idpru  6566  ltpopr  6568  ltexprlemopu  6576  ltexprlemdisj  6579  ltexprlemfl  6582  ltexprlemfu  6584  ltexprlemru  6585  recexprlemdisj  6601  recexprlemss1l  6606  recexprlemss1u  6607  cnegexlem1  6963  msqge0  7380  mulge0  7383  divnegap  7445  divdiv32ap  7458  divneg2ap  7474  peano2uz  8282  lbzbi  8307  expnlbnd  9006
  Copyright terms: Public domain W3C validator