Theorem sylbid 150

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

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbid.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr4d  203  ifnebibdc  3620  ssprsseq  3801  nlimsucg  4627  ssrelrn  4883  poltletr  5097  xp11m  5135  fvmptdf  5685  elfvmptrab1  5692  eusvobj2  5948  ovmpodf  6095  elovmporab  6164  elovmporab1w  6165  f1o2ndf1  6332  smoiso  6406  nnsseleq  6605  ecopovtrn  6737  ecopovtrng  6740  dom2lem  6881  fundmen  6917  fidifsnen  6988  findcard2  7007  findcard2s  7008  supisoex  7132  infglbti  7148  ordiso2  7158  updjud  7205  difinfsnlem  7222  enomnilem  7261  enmkvlem  7284  netap  7396  2omotaplemap  7399  cc2lem  7408  addcanpig  7477  mulcanpig  7478  addnidpig  7479  ordpipqqs  7517  ltexnqq  7551  prarloclemlo  7637  genpcdl  7662  genpcuu  7663  mulnqprl  7711  mulnqpru  7712  distrlem1prl  7725  distrlem1pru  7726  distrlem4prl  7727  distrlem4pru  7728  distrlem5prl  7729  distrlem5pru  7730  ltsopr  7739  ltexprlemfl  7752  ltexprlemfu  7754  recexprlemss1l  7778  recexprlemss1u  7779  aptiprleml  7782  ltsrprg  7890  lttrsr  7905  mulextsr1lem  7923  axapti  8173  cnegexlem1  8277  le2add  8547  lt2add  8548  ltleadd  8549  lt2sub  8563  le2sub  8564  recexre  8681  reapti  8682  apreap  8690  reapcotr  8701  remulext1  8702  apreim  8706  apcotr  8710  mulext2  8716  recexap  8756  addltmul  9304  elnnz  9412  zleloe  9449  difgtsumgt  9472  nn0n0n1ge2b  9482  nn0lt2  9484  nn0le2is012  9485  zextlt  9495  uzind2  9515  supinfneg  9746  infsupneg  9747  eluzdc  9761  qreccl  9793  elpq  9800  xltnegi  9987  xnn0lenn0nn0  10017  iccid  10077  icoshft  10142  zltaddlt1le  10159  fzofzim  10344  qbtwnxr  10432  flqeqceilz  10495  modqmuladdnn0  10545  modfzo0difsn  10572  addmodlteq  10575  frec2uzrand  10582  frecuzrdgtcl  10589  frecuzrdgfunlem  10596  seqf1oglem1  10696  facdiv  10915  facwordi  10917  faclbnd  10918  bcpasc  10943  seq3coll  11019  fundm2domnop0  11022  fstwrdne  11064  elovmpowrd  11067  lswlgt0cl  11078  ccatrn  11098  swrdnd  11145  swrdswrd  11191  wrd2ind  11209  recvguniq  11391  abs00ap  11458  absext  11459  absnid  11469  cau3lem  11510  climuni  11689  2clim  11697  summodc  11779  fisumss  11788  fsumabs  11861  mertenslem2  11932  fprodssdc  11986  reeff1  12096  efieq1re  12168  dvdsmultr2  12229  dvdsleabs  12241  odd2np1lem  12268  odd2np1  12269  ltoddhalfle  12289  halfleoddlt  12290  m1expo  12296  nn0enne  12298  nn0ehalf  12299  nn0o1gt2  12301  flodddiv4  12332  zeqzmulgcd  12376  gcdneg  12388  gcdaddm  12390  bezoutlemaz  12409  bezoutlembz  12410  dfgcd2  12420  gcddiv  12425  dvdssqim  12430  algcvgblem  12456  algcvga  12458  lcmneg  12481  coprmgcdb  12495  coprmdvds2  12500  qredeq  12503  divgcdcoprm0  12508  divgcdcoprmex  12509  cncongr1  12510  cncongr2  12511  prmind2  12527  dvdsnprmd  12532  prmgt1  12539  nprmdvds1  12547  divgcdodd  12550  euclemma  12553  prmdvdsexpr  12557  prmfac1  12559  prmndvdsfaclt  12563  crth  12631  eulerthlemh  12638  fermltl  12641  nnnn0modprm0  12663  coprimeprodsq2  12666  pythagtriplem2  12674  pcpremul  12701  pcdvdsb  12728  pc2dvds  12738  pc11  12739  dvdsprmpweqnn  12744  dvdsprmpweqle  12745  difsqpwdvds  12746  pcfac  12758  oddprmdvds  12762  prmpwdvds  12763  1arith  12775  4sqlem11  12809  4sqlem12  12810  imasaddfnlemg  13231  erlecpbl  13249  xpsff1o  13266  imasmnd2  13369  grp1inv  13524  imasgrp2  13531  ghmpreima  13687  imasabl  13757  imasrng  13803  imasring  13911  dvdsrtr  13948  dvdsrmul1  13949  unitgrp  13963  znidomb  14505  tgtop  14625  tgidm  14631  neipsm  14711  restbasg  14725  tgrest  14726  tgcn  14765  tgcnp  14766  cnconst2  14790  cnconst  14791  cnptopresti  14795  txbasval  14824  txcnp  14828  txdis1cn  14835  bldisj  14958  xblm  14974  blssps  14984  blss  14985  blin2  14989  cnlimcim  15228  dveflem  15283  sincosq3sgn  15385  sincosq4sgn  15386  coseq0q4123  15391  ioocosf1o  15411  logbgcd1irr  15524  mpodvdsmulf1o  15547  zabsle1  15561  lgsdir2lem5  15594  lgsne0  15600  lgsdirnn0  15609  gausslemma2dlem0i  15619  gausslemma2dlem1a  15620  gausslemma2dlem2  15624  gausslemma2dlem7  15630  gausslemma2d  15631  lgseisenlem2  15633  lgsquadlem1  15639  2lgslem1a1  15648  2lgslem1b  15651  2lgslem1c  15652  2lgs  15666  2lgsoddprmlem2  15668  upgrpredgv  15820  uzdcinzz  15904  dom1o  16098  subctctexmid  16109