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  3649  ssprsseq  3833  nlimsucg  4662  ssrelrn  4920  poltletr  5135  xp11m  5173  fvmptdf  5730  elfvmptrab1  5737  eusvobj2  5999  ovmpodf  6148  elovmporab  6217  elovmporab1w  6218  f1o2ndf1  6388  smoiso  6463  nnsseleq  6664  ecopovtrn  6796  ecopovtrng  6799  dom2lem  6940  fundmen  6976  dom1o  6997  fidifsnen  7052  findcard2  7071  findcard2s  7072  supisoex  7199  infglbti  7215  ordiso2  7225  updjud  7272  difinfsnlem  7289  enomnilem  7328  enmkvlem  7351  netap  7463  2omotaplemap  7466  cc2lem  7475  addcanpig  7544  mulcanpig  7545  addnidpig  7546  ordpipqqs  7584  ltexnqq  7618  prarloclemlo  7704  genpcdl  7729  genpcuu  7730  mulnqprl  7778  mulnqpru  7779  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  distrlem5prl  7796  distrlem5pru  7797  ltsopr  7806  ltexprlemfl  7819  ltexprlemfu  7821  recexprlemss1l  7845  recexprlemss1u  7846  aptiprleml  7849  ltsrprg  7957  lttrsr  7972  mulextsr1lem  7990  axapti  8240  cnegexlem1  8344  le2add  8614  lt2add  8615  ltleadd  8616  lt2sub  8630  le2sub  8631  recexre  8748  reapti  8749  apreap  8757  reapcotr  8768  remulext1  8769  apreim  8773  apcotr  8777  mulext2  8783  recexap  8823  addltmul  9371  elnnz  9479  zleloe  9516  difgtsumgt  9539  nn0n0n1ge2b  9549  nn0lt2  9551  nn0le2is012  9552  zextlt  9562  uzind2  9582  supinfneg  9819  infsupneg  9820  eluzdc  9834  qreccl  9866  elpq  9873  xltnegi  10060  xnn0lenn0nn0  10090  iccid  10150  icoshft  10215  zltaddlt1le  10232  fzofzim  10417  qbtwnxr  10507  flqeqceilz  10570  modqmuladdnn0  10620  modfzo0difsn  10647  addmodlteq  10650  frec2uzrand  10657  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  seqf1oglem1  10771  facdiv  10990  facwordi  10992  faclbnd  10993  bcpasc  11018  seq3coll  11096  fundm2domnop0  11099  fstwrdne  11142  elovmpowrd  11145  lswlgt0cl  11156  ccatrn  11176  ccatalpha  11180  swrdnd  11230  swrdswrd  11276  wrd2ind  11294  swrdccatin1  11296  pfxccatin12lem2a  11298  pfxccat3  11305  swrdccat  11306  swrdccat3blem  11310  reuccatpfxs1lem  11317  recvguniq  11546  abs00ap  11613  absext  11614  absnid  11624  cau3lem  11665  climuni  11844  2clim  11852  summodc  11934  fisumss  11943  fsumabs  12016  mertenslem2  12087  fprodssdc  12141  reeff1  12251  efieq1re  12323  dvdsmultr2  12384  dvdsleabs  12396  odd2np1lem  12423  odd2np1  12424  ltoddhalfle  12444  halfleoddlt  12445  m1expo  12451  nn0enne  12453  nn0ehalf  12454  nn0o1gt2  12456  flodddiv4  12487  zeqzmulgcd  12531  gcdneg  12543  gcdaddm  12545  bezoutlemaz  12564  bezoutlembz  12565  dfgcd2  12575  gcddiv  12580  dvdssqim  12585  algcvgblem  12611  algcvga  12613  lcmneg  12636  coprmgcdb  12650  coprmdvds2  12655  qredeq  12658  divgcdcoprm0  12663  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  prmind2  12682  dvdsnprmd  12687  prmgt1  12694  nprmdvds1  12702  divgcdodd  12705  euclemma  12708  prmdvdsexpr  12712  prmfac1  12714  prmndvdsfaclt  12718  crth  12786  eulerthlemh  12793  fermltl  12796  nnnn0modprm0  12818  coprimeprodsq2  12821  pythagtriplem2  12829  pcpremul  12856  pcdvdsb  12883  pc2dvds  12893  pc11  12894  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  difsqpwdvds  12901  pcfac  12913  oddprmdvds  12917  prmpwdvds  12918  1arith  12930  4sqlem11  12964  4sqlem12  12965  imasaddfnlemg  13387  erlecpbl  13405  xpsff1o  13422  imasmnd2  13525  grp1inv  13680  imasgrp2  13687  ghmpreima  13843  imasabl  13913  imasrng  13959  imasring  14067  dvdsrtr  14105  dvdsrmul1  14106  unitgrp  14120  znidomb  14662  tgtop  14782  tgidm  14788  neipsm  14868  restbasg  14882  tgrest  14883  tgcn  14922  tgcnp  14923  cnconst2  14947  cnconst  14948  cnptopresti  14952  txbasval  14981  txcnp  14985  txdis1cn  14992  bldisj  15115  xblm  15131  blssps  15141  blss  15142  blin2  15146  cnlimcim  15385  dveflem  15440  sincosq3sgn  15542  sincosq4sgn  15543  coseq0q4123  15548  ioocosf1o  15568  logbgcd1irr  15681  mpodvdsmulf1o  15704  zabsle1  15718  lgsdir2lem5  15751  lgsne0  15757  lgsdirnn0  15766  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem2  15790  lgsquadlem1  15796  2lgslem1a1  15805  2lgslem1b  15808  2lgslem1c  15809  2lgs  15823  2lgsoddprmlem2  15825  upgrpredgv  15985  ausgrumgrien  16009  ausgrusgrien  16010  usgruspgrben  16025  uhgr2edg  16045  usgredg4  16054  ushgredgedg  16065  ushgredgedgloop  16067  edg0usgr  16086  wlkl1loop  16155  wlk1walkdom  16156  wlklenvclwlk  16170  wlkres  16174  clwwlknonex2  16234  uzdcinzz  16330  subctctexmid  16537