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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  ifnebibdc  3686  ssprsseq  3877  nlimsucg  4713  ssrelrn  4972  poltletr  5188  xp11m  5226  fvmptdf  5793  elfvmptrab1  5801  eusvobj2  6071  ovmpodf  6220  elovmporab  6289  elovmporab1w  6290  f1o2ndf1  6464  suppssdc  6500  suppssrst  6501  suppssrgst  6502  smoiso  6573  nnsseleq  6774  ecopovtrn  6906  ecopovtrng  6909  dom2lem  7058  fundmen  7094  dom1o  7116  fidifsnen  7172  findcard2  7193  findcard2s  7194  supisoex  7349  infglbti  7365  ordiso2  7375  updjud  7422  difinfsnlem  7439  enomnilem  7478  enmkvlem  7501  netap  7620  2omotaplemap  7623  cc2lem  7632  addcanpig  7701  mulcanpig  7702  addnidpig  7703  ordpipqqs  7741  ltexnqq  7775  prarloclemlo  7861  genpcdl  7886  genpcuu  7887  mulnqprl  7935  mulnqpru  7936  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  distrlem5prl  7953  distrlem5pru  7954  ltsopr  7963  ltexprlemfl  7976  ltexprlemfu  7978  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  ltsrprg  8114  lttrsr  8129  mulextsr1lem  8147  axapti  8396  cnegexlem1  8501  le2add  8772  lt2add  8773  ltleadd  8774  lt2sub  8788  le2sub  8789  recexre  8906  reapti  8907  apreap  8915  reapcotr  8926  remulext1  8927  apreim  8931  apcotr  8935  mulext2  8941  recexap  8981  addltmul  9542  elnnz  9654  zleloe  9691  difgtsumgt  9714  nn0n0n1ge2b  9725  nn0lt2  9727  nn0le2is012  9728  zextlt  9738  uzind2  9758  supinfneg  9995  infsupneg  9996  eluzdc  10010  qreccl  10042  elpq  10049  xltnegi  10237  xnn0lenn0nn0  10267  iccid  10327  icoshft  10392  zltaddlt1le  10410  fzofzim  10600  qbtwnxr  10692  flqeqceilz  10755  modqmuladdnn0  10805  modfzo0difsn  10832  addmodlteq  10835  frec2uzrand  10842  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  seqf1oglem1  10956  facdiv  11176  facwordi  11178  faclbnd  11179  bcpasc  11204  seq3coll  11294  fundm2domnop0  11300  fstwrdne  11343  elovmpowrd  11346  lswlgt0cl  11357  ccatrn  11377  ccatalpha  11381  swrdnd  11431  swrdswrd  11477  wrd2ind  11495  swrdccatin1  11497  pfxccatin12lem2a  11499  pfxccat3  11506  swrdccat  11507  swrdccat3blem  11511  reuccatpfxs1lem  11518  recvguniq  11761  abs00ap  11828  absext  11829  absnid  11839  cau3lem  11880  climuni  12059  2clim  12067  summodc  12150  fisumss  12159  fsumabs  12232  mertenslem2  12303  fprodssdc  12357  reeff1  12467  efieq1re  12539  dvdsmultr2  12600  dvdsleabs  12612  odd2np1lem  12639  odd2np1  12640  ltoddhalfle  12660  halfleoddlt  12661  m1expo  12667  nn0enne  12669  nn0ehalf  12670  nn0o1gt2  12672  flodddiv4  12703  zeqzmulgcd  12747  gcdneg  12759  gcdaddm  12761  bezoutlemaz  12780  bezoutlembz  12781  dfgcd2  12791  gcddiv  12796  dvdssqim  12801  algcvgblem  12827  algcvga  12829  lcmneg  12852  coprmgcdb  12866  coprmdvds2  12871  qredeq  12874  divgcdcoprm0  12879  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  prmind2  12898  dvdsnprmd  12903  prmgt1  12910  nprmdvds1  12918  divgcdodd  12921  euclemma  12924  prmdvdsexpr  12928  prmfac1  12930  prmndvdsfaclt  12934  crth  13002  eulerthlemh  13009  fermltl  13012  nnnn0modprm0  13034  coprimeprodsq2  13037  pythagtriplem2  13045  pcpremul  13072  pcdvdsb  13099  pc2dvds  13109  pc11  13110  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  difsqpwdvds  13117  pcfac  13129  oddprmdvds  13133  prmpwdvds  13134  1arith  13146  4sqlem11  13180  4sqlem12  13181  ballotfilemfrceq  13272  imasaddfnlemg  13635  erlecpbl  13653  xpsff1o  13670  imasmnd2  13759  grp1inv  13912  imasgrp2  13913  ghmpreima  14069  imasabl  14140  imasrng  14255  imasring  14369  dvdsrtr  14408  dvdsrmul1  14409  unitgrp  14423  znidomb  14993  tgtop  15169  tgidm  15175  neipsm  15255  restbasg  15269  tgrest  15270  tgcn  15309  tgcnp  15310  cnconst2  15334  cnconst  15335  cnptopresti  15339  txbasval  15368  txcnp  15372  txdis1cn  15379  bldisj  15502  xblm  15518  blssps  15528  blss  15529  blin2  15533  cnlimcim  15772  dveflem  15827  sincosq3sgn  15929  sincosq4sgn  15930  coseq0q4123  15935  ioocosf1o  15955  logbgcd1irr  16069  birthdaylem1g  16087  pellexlem1  16091  pellexlem3  16093  mpodvdsmulf1o  16104  zabsle1  16118  lgsdir2lem5  16151  lgsne0  16157  lgsdirnn0  16166  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem7  16187  gausslemma2d  16188  lgseisenlem2  16190  lgsquadlem1  16196  2lgslem1a1  16205  2lgslem1b  16208  2lgslem1c  16209  2lgs  16223  2lgsoddprmlem2  16225  upgrpredgv  16387  ausgrumgrien  16411  ausgrusgrien  16412  usgruspgrben  16427  uhgr2edg  16447  usgredg4  16456  ushgredgedg  16467  ushgredgedgloop  16469  edg0usgr  16488  uhgrspansubgrlem  16517  wlkl1loop  16599  wlk1walkdom  16600  wlklenvclwlk  16614  wlkres  16620  clwwlknonex2  16680  uzdcinzz  16826  subctctexmid  17030