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  2764  eqsbc3r  2790  opeldmg  4458  elreldm  4478  ssimaex  5150  f1eqcocnv  5347  fliftfun  5352  isopolem  5377  isosolem  5379  brtposg  5782  issmo2  5817  rdgon  5884  frecsuclem3  5897  nnmcl  5966  nnawordi  5990  nnmordi  5991  nnmord  5992  swoord1  6037  ecopovtrn  6105  ecopovtrng  6108  enq0tr  6278  prubl  6329  ltexprlemloc  6433  addextpr  6445  recexprlem1ssl  6457  recexprlem1ssu  6458  mulcmpblnr  6482  mulgt0sr  6517  ltleletr  6703  ltle  6708  ltadd2  7018  leltadd  7043  reapti  7169  apreap  7177  reapcotr  7188  apcotr  7197  addext  7200  mulext1  7202  zapne  7886  zextle  7899  prime  7905  xrltle  8198  xrre2  8213  icc0r  8274
  Copyright terms: Public domain W3C validator