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  3600  nlimsucg  4598  poltletr  5066  xp11m  5104  fvmptdf  5645  elfvmptrab1  5652  eusvobj2  5904  ovmpodf  6050  elovmporab  6118  elovmporab1w  6119  f1o2ndf1  6281  smoiso  6355  nnsseleq  6554  ecopovtrn  6686  ecopovtrng  6689  dom2lem  6826  fundmen  6860  fidifsnen  6926  findcard2  6945  findcard2s  6946  supisoex  7068  infglbti  7084  ordiso2  7094  updjud  7141  difinfsnlem  7158  enomnilem  7197  enmkvlem  7220  netap  7314  2omotaplemap  7317  cc2lem  7326  addcanpig  7394  mulcanpig  7395  addnidpig  7396  ordpipqqs  7434  ltexnqq  7468  prarloclemlo  7554  genpcdl  7579  genpcuu  7580  mulnqprl  7628  mulnqpru  7629  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  distrlem5prl  7646  distrlem5pru  7647  ltsopr  7656  ltexprlemfl  7669  ltexprlemfu  7671  recexprlemss1l  7695  recexprlemss1u  7696  aptiprleml  7699  ltsrprg  7807  lttrsr  7822  mulextsr1lem  7840  axapti  8090  cnegexlem1  8194  le2add  8463  lt2add  8464  ltleadd  8465  lt2sub  8479  le2sub  8480  recexre  8597  reapti  8598  apreap  8606  reapcotr  8617  remulext1  8618  apreim  8622  apcotr  8626  mulext2  8632  recexap  8672  addltmul  9219  elnnz  9327  zleloe  9364  difgtsumgt  9386  nn0n0n1ge2b  9396  nn0lt2  9398  nn0le2is012  9399  zextlt  9409  uzind2  9429  supinfneg  9660  infsupneg  9661  eluzdc  9675  qreccl  9707  elpq  9714  xltnegi  9901  xnn0lenn0nn0  9931  iccid  9991  icoshft  10056  zltaddlt1le  10073  fzofzim  10255  qbtwnxr  10326  flqeqceilz  10389  modqmuladdnn0  10439  modfzo0difsn  10466  addmodlteq  10469  frec2uzrand  10476  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  seqf1oglem1  10590  facdiv  10809  facwordi  10811  faclbnd  10812  bcpasc  10837  seq3coll  10913  fstwrdne  10952  elovmpowrd  10955  recvguniq  11139  abs00ap  11206  absext  11207  absnid  11217  cau3lem  11258  climuni  11436  2clim  11444  summodc  11526  fisumss  11535  fsumabs  11608  mertenslem2  11679  fprodssdc  11733  reeff1  11843  efieq1re  11915  dvdsmultr2  11976  dvdsleabs  11987  odd2np1lem  12013  odd2np1  12014  ltoddhalfle  12034  halfleoddlt  12035  m1expo  12041  nn0enne  12043  nn0ehalf  12044  nn0o1gt2  12046  flodddiv4  12075  zeqzmulgcd  12107  gcdneg  12119  gcdaddm  12121  bezoutlemaz  12140  bezoutlembz  12141  dfgcd2  12151  gcddiv  12156  dvdssqim  12161  algcvgblem  12187  algcvga  12189  lcmneg  12212  coprmgcdb  12226  coprmdvds2  12231  qredeq  12234  divgcdcoprm0  12239  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  prmind2  12258  dvdsnprmd  12263  prmgt1  12270  nprmdvds1  12278  divgcdodd  12281  euclemma  12284  prmdvdsexpr  12288  prmfac1  12290  prmndvdsfaclt  12294  crth  12362  eulerthlemh  12369  fermltl  12372  nnnn0modprm0  12393  coprimeprodsq2  12396  pythagtriplem2  12404  pcpremul  12431  pcdvdsb  12458  pc2dvds  12468  pc11  12469  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  difsqpwdvds  12476  pcfac  12488  oddprmdvds  12492  prmpwdvds  12493  1arith  12505  4sqlem11  12539  4sqlem12  12540  imasaddfnlemg  12897  erlecpbl  12915  xpsff1o  12932  grp1inv  13179  imasgrp2  13180  ghmpreima  13336  imasabl  13406  imasrng  13452  imasring  13560  dvdsrtr  13597  dvdsrmul1  13598  unitgrp  13612  znidomb  14146  tgtop  14236  tgidm  14242  neipsm  14322  restbasg  14336  tgrest  14337  tgcn  14376  tgcnp  14377  cnconst2  14401  cnconst  14402  cnptopresti  14406  txbasval  14435  txcnp  14439  txdis1cn  14446  bldisj  14569  xblm  14585  blssps  14595  blss  14596  blin2  14600  cnlimcim  14825  dveflem  14872  sincosq3sgn  14963  sincosq4sgn  14964  coseq0q4123  14969  ioocosf1o  14989  logbgcd1irr  15099  zabsle1  15115  lgsdir2lem5  15148  lgsne0  15154  lgsdirnn0  15163  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem7  15184  gausslemma2d  15185  lgseisenlem2  15187  lgsquadlem1  15191  2lgsoddprmlem2  15194  uzdcinzz  15290  subctctexmid  15491