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  3655  ssprsseq  3840  nlimsucg  4670  ssrelrn  4928  poltletr  5144  xp11m  5182  fvmptdf  5743  elfvmptrab1  5750  eusvobj2  6014  ovmpodf  6163  elovmporab  6232  elovmporab1w  6233  f1o2ndf1  6402  suppssdc  6438  suppssrst  6439  suppssrgst  6440  smoiso  6511  nnsseleq  6712  ecopovtrn  6844  ecopovtrng  6847  dom2lem  6988  fundmen  7024  dom1o  7045  fidifsnen  7100  findcard2  7121  findcard2s  7122  supisoex  7251  infglbti  7267  ordiso2  7277  updjud  7324  difinfsnlem  7341  enomnilem  7380  enmkvlem  7403  netap  7516  2omotaplemap  7519  cc2lem  7528  addcanpig  7597  mulcanpig  7598  addnidpig  7599  ordpipqqs  7637  ltexnqq  7671  prarloclemlo  7757  genpcdl  7782  genpcuu  7783  mulnqprl  7831  mulnqpru  7832  distrlem1prl  7845  distrlem1pru  7846  distrlem4prl  7847  distrlem4pru  7848  distrlem5prl  7849  distrlem5pru  7850  ltsopr  7859  ltexprlemfl  7872  ltexprlemfu  7874  recexprlemss1l  7898  recexprlemss1u  7899  aptiprleml  7902  ltsrprg  8010  lttrsr  8025  mulextsr1lem  8043  axapti  8292  cnegexlem1  8396  le2add  8666  lt2add  8667  ltleadd  8668  lt2sub  8682  le2sub  8683  recexre  8800  reapti  8801  apreap  8809  reapcotr  8820  remulext1  8821  apreim  8825  apcotr  8829  mulext2  8835  recexap  8875  addltmul  9423  elnnz  9533  zleloe  9570  difgtsumgt  9593  nn0n0n1ge2b  9603  nn0lt2  9605  nn0le2is012  9606  zextlt  9616  uzind2  9636  supinfneg  9873  infsupneg  9874  eluzdc  9888  qreccl  9920  elpq  9927  xltnegi  10114  xnn0lenn0nn0  10144  iccid  10204  icoshft  10269  zltaddlt1le  10287  fzofzim  10473  qbtwnxr  10563  flqeqceilz  10626  modqmuladdnn0  10676  modfzo0difsn  10703  addmodlteq  10706  frec2uzrand  10713  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  seqf1oglem1  10827  facdiv  11046  facwordi  11048  faclbnd  11049  bcpasc  11074  seq3coll  11152  fundm2domnop0  11158  fstwrdne  11201  elovmpowrd  11204  lswlgt0cl  11215  ccatrn  11235  ccatalpha  11239  swrdnd  11289  swrdswrd  11335  wrd2ind  11353  swrdccatin1  11355  pfxccatin12lem2a  11357  pfxccat3  11364  swrdccat  11365  swrdccat3blem  11369  reuccatpfxs1lem  11376  recvguniq  11618  abs00ap  11685  absext  11686  absnid  11696  cau3lem  11737  climuni  11916  2clim  11924  summodc  12007  fisumss  12016  fsumabs  12089  mertenslem2  12160  fprodssdc  12214  reeff1  12324  efieq1re  12396  dvdsmultr2  12457  dvdsleabs  12469  odd2np1lem  12496  odd2np1  12497  ltoddhalfle  12517  halfleoddlt  12518  m1expo  12524  nn0enne  12526  nn0ehalf  12527  nn0o1gt2  12529  flodddiv4  12560  zeqzmulgcd  12604  gcdneg  12616  gcdaddm  12618  bezoutlemaz  12637  bezoutlembz  12638  dfgcd2  12648  gcddiv  12653  dvdssqim  12658  algcvgblem  12684  algcvga  12686  lcmneg  12709  coprmgcdb  12723  coprmdvds2  12728  qredeq  12731  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  prmind2  12755  dvdsnprmd  12760  prmgt1  12767  nprmdvds1  12775  divgcdodd  12778  euclemma  12781  prmdvdsexpr  12785  prmfac1  12787  prmndvdsfaclt  12791  crth  12859  eulerthlemh  12866  fermltl  12869  nnnn0modprm0  12891  coprimeprodsq2  12894  pythagtriplem2  12902  pcpremul  12929  pcdvdsb  12956  pc2dvds  12966  pc11  12967  dvdsprmpweqnn  12972  dvdsprmpweqle  12973  difsqpwdvds  12974  pcfac  12986  oddprmdvds  12990  prmpwdvds  12991  1arith  13003  4sqlem11  13037  4sqlem12  13038  imasaddfnlemg  13460  erlecpbl  13478  xpsff1o  13495  imasmnd2  13598  grp1inv  13753  imasgrp2  13760  ghmpreima  13916  imasabl  13986  imasrng  14033  imasring  14141  dvdsrtr  14179  dvdsrmul1  14180  unitgrp  14194  znidomb  14737  tgtop  14862  tgidm  14868  neipsm  14948  restbasg  14962  tgrest  14963  tgcn  15002  tgcnp  15003  cnconst2  15027  cnconst  15028  cnptopresti  15032  txbasval  15061  txcnp  15065  txdis1cn  15072  bldisj  15195  xblm  15211  blssps  15221  blss  15222  blin2  15226  cnlimcim  15465  dveflem  15520  sincosq3sgn  15622  sincosq4sgn  15623  coseq0q4123  15628  ioocosf1o  15648  logbgcd1irr  15761  pellexlem1  15774  pellexlem3  15776  mpodvdsmulf1o  15787  zabsle1  15801  lgsdir2lem5  15834  lgsne0  15840  lgsdirnn0  15849  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem2  15873  lgsquadlem1  15879  2lgslem1a1  15888  2lgslem1b  15891  2lgslem1c  15892  2lgs  15906  2lgsoddprmlem2  15908  upgrpredgv  16070  ausgrumgrien  16094  ausgrusgrien  16095  usgruspgrben  16110  uhgr2edg  16130  usgredg4  16139  ushgredgedg  16150  ushgredgedgloop  16152  edg0usgr  16171  uhgrspansubgrlem  16200  wlkl1loop  16282  wlk1walkdom  16283  wlklenvclwlk  16297  wlkres  16303  clwwlknonex2  16363  uzdcinzz  16499  subctctexmid  16705