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

Theorem sylbid 149
Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)
Hypotheses
Ref Expression
sylbid.1 (𝜑 → (𝜓𝜒))
sylbid.2 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
sylbid (𝜑 → (𝜓𝜃))

Proof of Theorem sylbid
StepHypRef Expression
1 sylbid.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpd 143 . 2 (𝜑 → (𝜓𝜒))
3 sylbid.2 . 2 (𝜑 → (𝜒𝜃))
42, 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
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3imtr4d  202  nlimsucg  4449  poltletr  4907  xp11m  4945  fvmptdf  5474  elfvmptrab1  5481  eusvobj2  5726  ovmpodf  5868  f1o2ndf1  6091  smoiso  6165  nnsseleq  6363  ecopovtrn  6492  ecopovtrng  6495  dom2lem  6632  fundmen  6666  fidifsnen  6730  findcard2  6749  findcard2s  6750  supisoex  6862  infglbti  6878  ordiso2  6886  updjud  6933  difinfsnlem  6950  enomnilem  6976  addcanpig  7106  mulcanpig  7107  addnidpig  7108  ordpipqqs  7146  ltexnqq  7180  prarloclemlo  7266  genpcdl  7291  genpcuu  7292  mulnqprl  7340  mulnqpru  7341  distrlem1prl  7354  distrlem1pru  7355  distrlem4prl  7356  distrlem4pru  7357  distrlem5prl  7358  distrlem5pru  7359  ltsopr  7368  ltexprlemfl  7381  ltexprlemfu  7383  recexprlemss1l  7407  recexprlemss1u  7408  aptiprleml  7411  ltsrprg  7519  lttrsr  7534  mulextsr1lem  7552  axapti  7799  cnegexlem1  7901  le2add  8170  lt2add  8171  ltleadd  8172  lt2sub  8186  le2sub  8187  recexre  8303  reapti  8304  apreap  8312  reapcotr  8323  remulext1  8324  apreim  8328  apcotr  8332  mulext2  8338  recexap  8377  addltmul  8910  elnnz  9018  zleloe  9055  nn0n0n1ge2b  9084  nn0lt2  9086  nn0le2is012  9087  zextlt  9097  uzind2  9117  supinfneg  9342  infsupneg  9343  eluzdc  9356  qreccl  9386  xltnegi  9569  xnn0lenn0nn0  9599  iccid  9659  icoshft  9724  zltaddlt1le  9740  fzofzim  9916  qbtwnxr  9986  flqeqceilz  10042  modqmuladdnn0  10092  modfzo0difsn  10119  addmodlteq  10122  frec2uzrand  10129  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  facdiv  10435  facwordi  10437  faclbnd  10438  bcpasc  10463  seq3coll  10536  recvguniq  10718  abs00ap  10785  absext  10786  absnid  10796  cau3lem  10837  climuni  11013  2clim  11021  summodc  11103  fisumss  11112  fsumabs  11185  mertenslem2  11256  reeff1  11317  efieq1re  11387  dvdsmultr2  11440  dvdsleabs  11450  odd2np1lem  11476  odd2np1  11477  ltoddhalfle  11497  halfleoddlt  11498  m1expo  11504  nn0enne  11506  nn0ehalf  11507  nn0o1gt2  11509  flodddiv4  11538  zeqzmulgcd  11566  gcdneg  11577  gcdaddm  11579  bezoutlemaz  11598  bezoutlembz  11599  dfgcd2  11609  gcddiv  11614  dvdssqim  11619  algcvgblem  11637  algcvga  11639  lcmneg  11662  coprmgcdb  11676  coprmdvds2  11681  qredeq  11684  divgcdcoprm0  11689  divgcdcoprmex  11690  cncongr1  11691  cncongr2  11692  prmind2  11708  dvdsnprmd  11713  prmgt1  11719  nprmdvds1  11727  divgcdodd  11728  euclemma  11731  prmdvdsexpr  11735  prmfac1  11737  prmndvdsfaclt  11741  crth  11806  tgtop  12143  tgidm  12149  neipsm  12229  restbasg  12243  tgrest  12244  tgcn  12283  tgcnp  12284  cnconst2  12308  cnconst  12309  cnptopresti  12313  txbasval  12342  txcnp  12346  txdis1cn  12353  bldisj  12476  xblm  12492  blssps  12502  blss  12503  blin2  12507  cnlimcim  12715  dveflem  12761  uzdcinzz  12839  subctctexmid  13030
  Copyright terms: Public domain W3C validator