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  3648  ssprsseq  3829  nlimsucg  4657  ssrelrn  4913  poltletr  5128  xp11m  5166  fvmptdf  5721  elfvmptrab1  5728  eusvobj2  5986  ovmpodf  6135  elovmporab  6204  elovmporab1w  6205  f1o2ndf1  6372  smoiso  6446  nnsseleq  6645  ecopovtrn  6777  ecopovtrng  6780  dom2lem  6921  fundmen  6957  fidifsnen  7028  findcard2  7047  findcard2s  7048  supisoex  7172  infglbti  7188  ordiso2  7198  updjud  7245  difinfsnlem  7262  enomnilem  7301  enmkvlem  7324  netap  7436  2omotaplemap  7439  cc2lem  7448  addcanpig  7517  mulcanpig  7518  addnidpig  7519  ordpipqqs  7557  ltexnqq  7591  prarloclemlo  7677  genpcdl  7702  genpcuu  7703  mulnqprl  7751  mulnqpru  7752  distrlem1prl  7765  distrlem1pru  7766  distrlem4prl  7767  distrlem4pru  7768  distrlem5prl  7769  distrlem5pru  7770  ltsopr  7779  ltexprlemfl  7792  ltexprlemfu  7794  recexprlemss1l  7818  recexprlemss1u  7819  aptiprleml  7822  ltsrprg  7930  lttrsr  7945  mulextsr1lem  7963  axapti  8213  cnegexlem1  8317  le2add  8587  lt2add  8588  ltleadd  8589  lt2sub  8603  le2sub  8604  recexre  8721  reapti  8722  apreap  8730  reapcotr  8741  remulext1  8742  apreim  8746  apcotr  8750  mulext2  8756  recexap  8796  addltmul  9344  elnnz  9452  zleloe  9489  difgtsumgt  9512  nn0n0n1ge2b  9522  nn0lt2  9524  nn0le2is012  9525  zextlt  9535  uzind2  9555  supinfneg  9786  infsupneg  9787  eluzdc  9801  qreccl  9833  elpq  9840  xltnegi  10027  xnn0lenn0nn0  10057  iccid  10117  icoshft  10182  zltaddlt1le  10199  fzofzim  10384  qbtwnxr  10472  flqeqceilz  10535  modqmuladdnn0  10585  modfzo0difsn  10612  addmodlteq  10615  frec2uzrand  10622  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  seqf1oglem1  10736  facdiv  10955  facwordi  10957  faclbnd  10958  bcpasc  10983  seq3coll  11059  fundm2domnop0  11062  fstwrdne  11105  elovmpowrd  11108  lswlgt0cl  11119  ccatrn  11139  swrdnd  11186  swrdswrd  11232  wrd2ind  11250  swrdccatin1  11252  pfxccatin12lem2a  11254  pfxccat3  11261  swrdccat  11262  swrdccat3blem  11266  reuccatpfxs1lem  11273  recvguniq  11501  abs00ap  11568  absext  11569  absnid  11579  cau3lem  11620  climuni  11799  2clim  11807  summodc  11889  fisumss  11898  fsumabs  11971  mertenslem2  12042  fprodssdc  12096  reeff1  12206  efieq1re  12278  dvdsmultr2  12339  dvdsleabs  12351  odd2np1lem  12378  odd2np1  12379  ltoddhalfle  12399  halfleoddlt  12400  m1expo  12406  nn0enne  12408  nn0ehalf  12409  nn0o1gt2  12411  flodddiv4  12442  zeqzmulgcd  12486  gcdneg  12498  gcdaddm  12500  bezoutlemaz  12519  bezoutlembz  12520  dfgcd2  12530  gcddiv  12535  dvdssqim  12540  algcvgblem  12566  algcvga  12568  lcmneg  12591  coprmgcdb  12605  coprmdvds2  12610  qredeq  12613  divgcdcoprm0  12618  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  prmind2  12637  dvdsnprmd  12642  prmgt1  12649  nprmdvds1  12657  divgcdodd  12660  euclemma  12663  prmdvdsexpr  12667  prmfac1  12669  prmndvdsfaclt  12673  crth  12741  eulerthlemh  12748  fermltl  12751  nnnn0modprm0  12773  coprimeprodsq2  12776  pythagtriplem2  12784  pcpremul  12811  pcdvdsb  12838  pc2dvds  12848  pc11  12849  dvdsprmpweqnn  12854  dvdsprmpweqle  12855  difsqpwdvds  12856  pcfac  12868  oddprmdvds  12872  prmpwdvds  12873  1arith  12885  4sqlem11  12919  4sqlem12  12920  imasaddfnlemg  13342  erlecpbl  13360  xpsff1o  13377  imasmnd2  13480  grp1inv  13635  imasgrp2  13642  ghmpreima  13798  imasabl  13868  imasrng  13914  imasring  14022  dvdsrtr  14059  dvdsrmul1  14060  unitgrp  14074  znidomb  14616  tgtop  14736  tgidm  14742  neipsm  14822  restbasg  14836  tgrest  14837  tgcn  14876  tgcnp  14877  cnconst2  14901  cnconst  14902  cnptopresti  14906  txbasval  14935  txcnp  14939  txdis1cn  14946  bldisj  15069  xblm  15085  blssps  15095  blss  15096  blin2  15100  cnlimcim  15339  dveflem  15394  sincosq3sgn  15496  sincosq4sgn  15497  coseq0q4123  15502  ioocosf1o  15522  logbgcd1irr  15635  mpodvdsmulf1o  15658  zabsle1  15672  lgsdir2lem5  15705  lgsne0  15711  lgsdirnn0  15720  gausslemma2dlem0i  15730  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem7  15741  gausslemma2d  15742  lgseisenlem2  15744  lgsquadlem1  15750  2lgslem1a1  15759  2lgslem1b  15762  2lgslem1c  15763  2lgs  15777  2lgsoddprmlem2  15779  upgrpredgv  15938  ausgrumgrien  15962  ausgrusgrien  15963  usgruspgrben  15978  uhgr2edg  15998  usgredg4  16007  ushgredgedg  16018  ushgredgedgloop  16020  uzdcinzz  16120  dom1o  16314  subctctexmid  16325