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

Theorem sylibrd 158
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylibrd.1 (φ → (ψχ))
sylibrd.2 (φ → (θχ))
Assertion
Ref Expression
sylibrd (φ → (ψθ))

Proof of Theorem sylibrd
StepHypRef Expression
1 sylibrd.1 . 2 (φ → (ψχ))
2 sylibrd.2 . . 3 (φ → (θχ))
32biimprd 147 . 2 (φ → (χθ))
41, 3syld 40 1 (φ → (ψθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
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
This theorem is referenced by:  3imtr4d  192  sbciegft  2766  eqsbc3r  2792  opeldmg  4463  elreldm  4483  ssimaex  5155  f1eqcocnv  5352  fliftfun  5357  isopolem  5382  isosolem  5384  brtposg  5787  issmo2  5822  rdgon  5889  frecsuclem3  5902  nnmcl  5971  nnawordi  5995  nnmordi  5996  nnmord  5997  swoord1  6042  ecopovtrn  6110  ecopovtrng  6113  enq0tr  6283  prubl  6334  ltexprlemloc  6438  recexprlem1ssl  6461  recexprlem1ssu  6462  mulcmpblnr  6482  mulgt0sr  6516  ltleletr  6692  ltle  6697  ltadd2  7002  leltadd  7027
  Copyright terms: Public domain W3C validator