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  3605  nlimsucg  4603  poltletr  5071  xp11m  5109  fvmptdf  5652  elfvmptrab1  5659  eusvobj2  5911  ovmpodf  6058  elovmporab  6127  elovmporab1w  6128  f1o2ndf1  6290  smoiso  6364  nnsseleq  6563  ecopovtrn  6695  ecopovtrng  6698  dom2lem  6835  fundmen  6869  fidifsnen  6935  findcard2  6954  findcard2s  6955  supisoex  7079  infglbti  7095  ordiso2  7105  updjud  7152  difinfsnlem  7169  enomnilem  7208  enmkvlem  7231  netap  7326  2omotaplemap  7329  cc2lem  7338  addcanpig  7406  mulcanpig  7407  addnidpig  7408  ordpipqqs  7446  ltexnqq  7480  prarloclemlo  7566  genpcdl  7591  genpcuu  7592  mulnqprl  7640  mulnqpru  7641  distrlem1prl  7654  distrlem1pru  7655  distrlem4prl  7656  distrlem4pru  7657  distrlem5prl  7658  distrlem5pru  7659  ltsopr  7668  ltexprlemfl  7681  ltexprlemfu  7683  recexprlemss1l  7707  recexprlemss1u  7708  aptiprleml  7711  ltsrprg  7819  lttrsr  7834  mulextsr1lem  7852  axapti  8102  cnegexlem1  8206  le2add  8476  lt2add  8477  ltleadd  8478  lt2sub  8492  le2sub  8493  recexre  8610  reapti  8611  apreap  8619  reapcotr  8630  remulext1  8631  apreim  8635  apcotr  8639  mulext2  8645  recexap  8685  addltmul  9233  elnnz  9341  zleloe  9378  difgtsumgt  9400  nn0n0n1ge2b  9410  nn0lt2  9412  nn0le2is012  9413  zextlt  9423  uzind2  9443  supinfneg  9674  infsupneg  9675  eluzdc  9689  qreccl  9721  elpq  9728  xltnegi  9915  xnn0lenn0nn0  9945  iccid  10005  icoshft  10070  zltaddlt1le  10087  fzofzim  10269  qbtwnxr  10352  flqeqceilz  10415  modqmuladdnn0  10465  modfzo0difsn  10492  addmodlteq  10495  frec2uzrand  10502  frecuzrdgtcl  10509  frecuzrdgfunlem  10516  seqf1oglem1  10616  facdiv  10835  facwordi  10837  faclbnd  10838  bcpasc  10863  seq3coll  10939  fstwrdne  10978  elovmpowrd  10981  recvguniq  11165  abs00ap  11232  absext  11233  absnid  11243  cau3lem  11284  climuni  11463  2clim  11471  summodc  11553  fisumss  11562  fsumabs  11635  mertenslem2  11706  fprodssdc  11760  reeff1  11870  efieq1re  11942  dvdsmultr2  12003  dvdsleabs  12015  odd2np1lem  12042  odd2np1  12043  ltoddhalfle  12063  halfleoddlt  12064  m1expo  12070  nn0enne  12072  nn0ehalf  12073  nn0o1gt2  12075  flodddiv4  12106  zeqzmulgcd  12150  gcdneg  12162  gcdaddm  12164  bezoutlemaz  12183  bezoutlembz  12184  dfgcd2  12194  gcddiv  12199  dvdssqim  12204  algcvgblem  12230  algcvga  12232  lcmneg  12255  coprmgcdb  12269  coprmdvds2  12274  qredeq  12277  divgcdcoprm0  12282  divgcdcoprmex  12283  cncongr1  12284  cncongr2  12285  prmind2  12301  dvdsnprmd  12306  prmgt1  12313  nprmdvds1  12321  divgcdodd  12324  euclemma  12327  prmdvdsexpr  12331  prmfac1  12333  prmndvdsfaclt  12337  crth  12405  eulerthlemh  12412  fermltl  12415  nnnn0modprm0  12437  coprimeprodsq2  12440  pythagtriplem2  12448  pcpremul  12475  pcdvdsb  12502  pc2dvds  12512  pc11  12513  dvdsprmpweqnn  12518  dvdsprmpweqle  12519  difsqpwdvds  12520  pcfac  12532  oddprmdvds  12536  prmpwdvds  12537  1arith  12549  4sqlem11  12583  4sqlem12  12584  imasaddfnlemg  13004  erlecpbl  13022  xpsff1o  13039  grp1inv  13286  imasgrp2  13287  ghmpreima  13443  imasabl  13513  imasrng  13559  imasring  13667  dvdsrtr  13704  dvdsrmul1  13705  unitgrp  13719  znidomb  14261  tgtop  14351  tgidm  14357  neipsm  14437  restbasg  14451  tgrest  14452  tgcn  14491  tgcnp  14492  cnconst2  14516  cnconst  14517  cnptopresti  14521  txbasval  14550  txcnp  14554  txdis1cn  14561  bldisj  14684  xblm  14700  blssps  14710  blss  14711  blin2  14715  cnlimcim  14954  dveflem  15009  sincosq3sgn  15111  sincosq4sgn  15112  coseq0q4123  15117  ioocosf1o  15137  logbgcd1irr  15250  mpodvdsmulf1o  15273  zabsle1  15287  lgsdir2lem5  15320  lgsne0  15326  lgsdirnn0  15335  gausslemma2dlem0i  15345  gausslemma2dlem1a  15346  gausslemma2dlem2  15350  gausslemma2dlem7  15356  gausslemma2d  15357  lgseisenlem2  15359  lgsquadlem1  15365  2lgslem1a1  15374  2lgslem1b  15377  2lgslem1c  15378  2lgs  15392  2lgsoddprmlem2  15394  uzdcinzz  15491  subctctexmid  15694