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

Theorem sylibrd 168
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 157 . 2 (𝜑 → (𝜒𝜃))
41, 3syld 45 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr4d  202  sbciegft  2942  opeldmg  4751  elreldm  4772  ssimaex  5489  resflem  5591  f1eqcocnv  5699  fliftfun  5704  isopolem  5730  isosolem  5732  brtposg  6158  issmo2  6193  nnmcl  6384  nnawordi  6418  nnmordi  6419  nnmord  6420  swoord1  6465  ecopovtrn  6533  ecopovtrng  6536  f1domg  6659  mapen  6747  mapxpen  6749  supmoti  6887  isotilem  6900  exmidomniim  7020  enq0tr  7265  prubl  7317  ltexprlemloc  7438  addextpr  7452  recexprlem1ssl  7464  recexprlem1ssu  7465  cauappcvgprlemdisj  7482  mulcmpblnr  7572  mulgt0sr  7609  map2psrprg  7636  ltleletr  7869  ltle  7874  ltadd2  8204  leltadd  8232  reapti  8364  apreap  8372  reapcotr  8383  apcotr  8392  addext  8395  mulext1  8397  cnstab  8430  zapne  9148  zextle  9165  prime  9173  uzin  9381  indstr  9414  supinfneg  9416  infsupneg  9417  ublbneg  9431  xrltle  9613  xrre2  9633  icc0r  9738  fzrevral  9915  flqge  10085  modqadd1  10164  modqmul1  10180  facdiv  10515  resqrexlemgt0  10823  abs00ap  10865  absext  10866  climshftlemg  11102  climcaucn  11151  dvds2lem  11539  dvdsfac  11592  ltoddhalfle  11624  ndvdsadd  11662  gcdaddm  11706  bezoutlembi  11727  gcdzeq  11744  algcvga  11766  rpdvds  11814  cncongr1  11818  cncongr2  11819  prmind2  11835  euclemma  11858  isprm6  11859  rpexp  11865  sqrt2irr  11874  fiinbas  12253  bastg  12267  tgcl  12270  opnssneib  12362  tgcnp  12415  iscnp4  12424  cnntr  12431  cnptopresti  12444  lmss  12452  lmtopcnp  12456  txdis  12483  xblss2ps  12610  xblss2  12611  blsscls2  12699  metequiv2  12702  bdxmet  12707  mulc1cncf  12782  cncfco  12784  sincosq2sgn  12954  sincosq3sgn  12955  sincosq4sgn  12956  triap  13397
  Copyright terms: Public domain W3C validator