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  3614  nlimsucg  4613  poltletr  5082  xp11m  5120  fvmptdf  5666  elfvmptrab1  5673  eusvobj2  5929  ovmpodf  6076  elovmporab  6145  elovmporab1w  6146  f1o2ndf1  6313  smoiso  6387  nnsseleq  6586  ecopovtrn  6718  ecopovtrng  6721  dom2lem  6862  fundmen  6897  fidifsnen  6966  findcard2  6985  findcard2s  6986  supisoex  7110  infglbti  7126  ordiso2  7136  updjud  7183  difinfsnlem  7200  enomnilem  7239  enmkvlem  7262  netap  7365  2omotaplemap  7368  cc2lem  7377  addcanpig  7446  mulcanpig  7447  addnidpig  7448  ordpipqqs  7486  ltexnqq  7520  prarloclemlo  7606  genpcdl  7631  genpcuu  7632  mulnqprl  7680  mulnqpru  7681  distrlem1prl  7694  distrlem1pru  7695  distrlem4prl  7696  distrlem4pru  7697  distrlem5prl  7698  distrlem5pru  7699  ltsopr  7708  ltexprlemfl  7721  ltexprlemfu  7723  recexprlemss1l  7747  recexprlemss1u  7748  aptiprleml  7751  ltsrprg  7859  lttrsr  7874  mulextsr1lem  7892  axapti  8142  cnegexlem1  8246  le2add  8516  lt2add  8517  ltleadd  8518  lt2sub  8532  le2sub  8533  recexre  8650  reapti  8651  apreap  8659  reapcotr  8670  remulext1  8671  apreim  8675  apcotr  8679  mulext2  8685  recexap  8725  addltmul  9273  elnnz  9381  zleloe  9418  difgtsumgt  9441  nn0n0n1ge2b  9451  nn0lt2  9453  nn0le2is012  9454  zextlt  9464  uzind2  9484  supinfneg  9715  infsupneg  9716  eluzdc  9730  qreccl  9762  elpq  9769  xltnegi  9956  xnn0lenn0nn0  9986  iccid  10046  icoshft  10111  zltaddlt1le  10128  fzofzim  10310  qbtwnxr  10398  flqeqceilz  10461  modqmuladdnn0  10511  modfzo0difsn  10538  addmodlteq  10541  frec2uzrand  10548  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  seqf1oglem1  10662  facdiv  10881  facwordi  10883  faclbnd  10884  bcpasc  10909  seq3coll  10985  fundm2domnop0  10988  fstwrdne  11030  elovmpowrd  11033  lswlgt0cl  11043  ccatrn  11063  recvguniq  11277  abs00ap  11344  absext  11345  absnid  11355  cau3lem  11396  climuni  11575  2clim  11583  summodc  11665  fisumss  11674  fsumabs  11747  mertenslem2  11818  fprodssdc  11872  reeff1  11982  efieq1re  12054  dvdsmultr2  12115  dvdsleabs  12127  odd2np1lem  12154  odd2np1  12155  ltoddhalfle  12175  halfleoddlt  12176  m1expo  12182  nn0enne  12184  nn0ehalf  12185  nn0o1gt2  12187  flodddiv4  12218  zeqzmulgcd  12262  gcdneg  12274  gcdaddm  12276  bezoutlemaz  12295  bezoutlembz  12296  dfgcd2  12306  gcddiv  12311  dvdssqim  12316  algcvgblem  12342  algcvga  12344  lcmneg  12367  coprmgcdb  12381  coprmdvds2  12386  qredeq  12389  divgcdcoprm0  12394  divgcdcoprmex  12395  cncongr1  12396  cncongr2  12397  prmind2  12413  dvdsnprmd  12418  prmgt1  12425  nprmdvds1  12433  divgcdodd  12436  euclemma  12439  prmdvdsexpr  12443  prmfac1  12445  prmndvdsfaclt  12449  crth  12517  eulerthlemh  12524  fermltl  12527  nnnn0modprm0  12549  coprimeprodsq2  12552  pythagtriplem2  12560  pcpremul  12587  pcdvdsb  12614  pc2dvds  12624  pc11  12625  dvdsprmpweqnn  12630  dvdsprmpweqle  12631  difsqpwdvds  12632  pcfac  12644  oddprmdvds  12648  prmpwdvds  12649  1arith  12661  4sqlem11  12695  4sqlem12  12696  imasaddfnlemg  13117  erlecpbl  13135  xpsff1o  13152  imasmnd2  13255  grp1inv  13410  imasgrp2  13417  ghmpreima  13573  imasabl  13643  imasrng  13689  imasring  13797  dvdsrtr  13834  dvdsrmul1  13835  unitgrp  13849  znidomb  14391  tgtop  14511  tgidm  14517  neipsm  14597  restbasg  14611  tgrest  14612  tgcn  14651  tgcnp  14652  cnconst2  14676  cnconst  14677  cnptopresti  14681  txbasval  14710  txcnp  14714  txdis1cn  14721  bldisj  14844  xblm  14860  blssps  14870  blss  14871  blin2  14875  cnlimcim  15114  dveflem  15169  sincosq3sgn  15271  sincosq4sgn  15272  coseq0q4123  15277  ioocosf1o  15297  logbgcd1irr  15410  mpodvdsmulf1o  15433  zabsle1  15447  lgsdir2lem5  15480  lgsne0  15486  lgsdirnn0  15495  gausslemma2dlem0i  15505  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  gausslemma2dlem7  15516  gausslemma2d  15517  lgseisenlem2  15519  lgsquadlem1  15525  2lgslem1a1  15534  2lgslem1b  15537  2lgslem1c  15538  2lgs  15552  2lgsoddprmlem2  15554  uzdcinzz  15696  subctctexmid  15899