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

Theorem sylibrd 167
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 156 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 44 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr4d  201  sbciegft  2845  opeldmg  4568  elreldm  4588  ssimaex  5266  f1eqcocnv  5462  fliftfun  5467  isopolem  5492  isosolem  5494  brtposg  5903  issmo2  5938  nnmcl  6125  nnawordi  6154  nnmordi  6155  nnmord  6156  swoord1  6201  ecopovtrn  6269  ecopovtrng  6272  f1domg  6305  supmoti  6465  isotilem  6478  enq0tr  6686  prubl  6738  ltexprlemloc  6859  addextpr  6873  recexprlem1ssl  6885  recexprlem1ssu  6886  cauappcvgprlemdisj  6903  mulcmpblnr  6980  mulgt0sr  7016  ltleletr  7260  ltle  7265  ltadd2  7590  leltadd  7618  reapti  7746  apreap  7754  reapcotr  7765  apcotr  7774  addext  7777  mulext1  7779  zapne  8503  zextle  8519  prime  8527  uzin  8732  indstr  8762  supinfneg  8764  infsupneg  8765  ublbneg  8779  xrltle  8949  xrre2  8964  icc0r  9025  fzrevral  9198  flqge  9364  modqadd1  9443  modqmul1  9459  facdiv  9762  resqrexlemgt0  10044  abs00ap  10086  absext  10087  climshftlemg  10279  climcaucn  10326  dvds2lem  10352  dvdsfac  10405  ltoddhalfle  10437  ndvdsadd  10475  gcdaddm  10519  bezoutlembi  10538  gcdzeq  10555  ialgcvga  10577  rpdvds  10625  cncongr1  10629  cncongr2  10630  prmind2  10646  euclemma  10669  isprm6  10670  rpexp  10676  sqrt2irr  10685
  Copyright terms: Public domain W3C validator