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

Theorem sylbid 148
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 142 . 2 (𝜑 → (𝜓𝜒))
3 sylbid.2 . 2 (𝜑 → (𝜒𝜃))
42, 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
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr4d  201  nlimsucg  4317  poltletr  4755  xp11m  4789  fvmptdf  5290  eusvobj2  5529  ovmpt2df  5663  f1o2ndf1  5880  smoiso  5951  nnsseleq  6145  ecopovtrn  6269  ecopovtrng  6272  dom2lem  6319  fundmen  6353  fidifsnen  6405  findcard2  6423  findcard2s  6424  supisoex  6481  infglbti  6497  ordiso2  6505  addcanpig  6586  mulcanpig  6587  addnidpig  6588  ordpipqqs  6626  ltexnqq  6660  prarloclemlo  6746  genpcdl  6771  genpcuu  6772  mulnqprl  6820  mulnqpru  6821  distrlem1prl  6834  distrlem1pru  6835  distrlem4prl  6836  distrlem4pru  6837  distrlem5prl  6838  distrlem5pru  6839  ltsopr  6848  ltexprlemfl  6861  ltexprlemfu  6863  recexprlemss1l  6887  recexprlemss1u  6888  aptiprleml  6891  ltsrprg  6986  lttrsr  7001  mulextsr1lem  7018  axapti  7250  cnegexlem1  7350  le2add  7615  lt2add  7616  ltleadd  7617  lt2sub  7631  le2sub  7632  recexre  7745  reapti  7746  apreap  7754  reapcotr  7765  remulext1  7766  apreim  7770  apcotr  7774  mulext2  7780  recexap  7810  addltmul  8334  elnnz  8442  zleloe  8479  nn0n0n1ge2b  8508  nn0lt2  8510  zextlt  8520  uzind2  8540  supinfneg  8764  infsupneg  8765  eluzdc  8778  qreccl  8808  xltnegi  8978  iccid  9024  icoshft  9088  zltaddlt1le  9104  fzofzim  9274  qbtwnxr  9344  flqeqceilz  9400  modqmuladdnn0  9450  modfzo0difsn  9477  addmodlteq  9480  frec2uzrand  9487  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  facdiv  9762  facwordi  9764  faclbnd  9765  bcpasc  9790  recvguniq  10019  abs00ap  10086  absext  10087  absnid  10097  cau3lem  10138  climuni  10270  2clim  10278  dvdsmultr2  10380  dvdsleabs  10390  odd2np1lem  10416  odd2np1  10417  ltoddhalfle  10437  halfleoddlt  10438  m1expo  10444  nn0enne  10446  nn0ehalf  10447  nn0o1gt2  10449  flodddiv4  10478  zeqzmulgcd  10506  gcdneg  10517  gcdaddm  10519  bezoutlemaz  10536  bezoutlembz  10537  dfgcd2  10547  gcddiv  10552  dvdssqim  10557  algcvgblem  10575  ialgcvga  10577  lcmneg  10600  coprmgcdb  10614  coprmdvds2  10619  qredeq  10622  divgcdcoprm0  10627  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  prmind2  10646  dvdsnprmd  10651  prmgt1  10657  nprmdvds1  10665  divgcdodd  10666  euclemma  10669  prmdvdsexpr  10673  prmfac1  10675  prmndvdsfaclt  10679  uzdcinzz  10759
  Copyright terms: Public domain W3C validator