ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylibrd 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  2793  eqsbc3r  2819  opeldmg  4540  elreldm  4560  ssimaex  5234  f1eqcocnv  5431  fliftfun  5436  isopolem  5461  isosolem  5463  brtposg  5869  issmo2  5904  rdgon  5973  frecsuclem3  5990  freccl  5993  nnmcl  6060  nnawordi  6088  nnmordi  6089  nnmord  6090  swoord1  6135  ecopovtrn  6203  ecopovtrng  6206  f1domg  6238  enq0tr  6532  prubl  6584  ltexprlemloc  6705  addextpr  6719  recexprlem1ssl  6731  recexprlem1ssu  6732  cauappcvgprlemdisj  6749  mulcmpblnr  6826  mulgt0sr  6862  ltleletr  7100  ltle  7105  ltadd2  7416  leltadd  7442  reapti  7570  apreap  7578  reapcotr  7589  apcotr  7598  addext  7601  mulext1  7603  zapne  8315  zextle  8331  prime  8337  uzin  8505  indstr  8536  ublbneg  8548  xrltle  8719  xrre2  8734  icc0r  8795  fzrevral  8967  flqge  9124  resqrexlemgt0  9618  abs00ap  9660  absext  9661  climshftlemg  9823  climcaucn  9870  sqrt2irr  9878  ialgcvga  9890
  Copyright terms: Public domain W3C validator