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  2787  eqsbc3r  2813  opeldmg  4483  elreldm  4503  ssimaex  5177  f1eqcocnv  5374  fliftfun  5379  isopolem  5404  isosolem  5406  brtposg  5810  issmo2  5845  rdgon  5913  frecsuclem3  5929  freccl  5932  nnmcl  5999  nnawordi  6024  nnmordi  6025  nnmord  6026  swoord1  6071  ecopovtrn  6139  ecopovtrng  6142  f1domg  6174  enq0tr  6416  prubl  6468  ltexprlemloc  6579  addextpr  6591  recexprlem1ssl  6603  recexprlem1ssu  6604  mulcmpblnr  6629  mulgt0sr  6664  ltleletr  6857  ltle  6862  ltadd2  7172  leltadd  7197  reapti  7323  apreap  7331  reapcotr  7342  apcotr  7351  addext  7354  mulext1  7356  zapne  8051  zextle  8067  prime  8073  uzin  8241  indstr  8272  ublbneg  8284  xrltle  8449  xrre2  8464  icc0r  8525  fzrevral  8697
  Copyright terms: Public domain W3C validator