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  6580  addextpr  6592  recexprlem1ssl  6604  recexprlem1ssu  6605  cauappcvgprlemdisj  6622  mulcmpblnr  6649  mulgt0sr  6684  ltleletr  6877  ltle  6882  ltadd2  7192  leltadd  7217  reapti  7343  apreap  7351  reapcotr  7362  apcotr  7371  addext  7374  mulext1  7376  zapne  8071  zextle  8087  prime  8093  uzin  8261  indstr  8292  ublbneg  8304  xrltle  8469  xrre2  8484  icc0r  8545  fzrevral  8717
  Copyright terms: Public domain W3C validator