Theorem sylbid 149

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 143	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbid.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  nlimsucg  4523  poltletr  4983  xp11m  5021  fvmptdf  5552  elfvmptrab1  5559  eusvobj2  5804  ovmpodf  5946  f1o2ndf1  6169  smoiso  6243  nnsseleq  6441  ecopovtrn  6570  ecopovtrng  6573  dom2lem  6710  fundmen  6744  fidifsnen  6808  findcard2  6827  findcard2s  6828  supisoex  6945  infglbti  6961  ordiso2  6969  updjud  7016  difinfsnlem  7033  enomnilem  7064  enmkvlem  7087  cc2lem  7169  addcanpig  7237  mulcanpig  7238  addnidpig  7239  ordpipqqs  7277  ltexnqq  7311  prarloclemlo  7397  genpcdl  7422  genpcuu  7423  mulnqprl  7471  mulnqpru  7472  distrlem1prl  7485  distrlem1pru  7486  distrlem4prl  7487  distrlem4pru  7488  distrlem5prl  7489  distrlem5pru  7490  ltsopr  7499  ltexprlemfl  7512  ltexprlemfu  7514  recexprlemss1l  7538  recexprlemss1u  7539  aptiprleml  7542  ltsrprg  7650  lttrsr  7665  mulextsr1lem  7683  axapti  7931  cnegexlem1  8033  le2add  8302  lt2add  8303  ltleadd  8304  lt2sub  8318  le2sub  8319  recexre  8436  reapti  8437  apreap  8445  reapcotr  8456  remulext1  8457  apreim  8461  apcotr  8465  mulext2  8471  recexap  8510  addltmul  9052  elnnz  9160  zleloe  9197  nn0n0n1ge2b  9226  nn0lt2  9228  nn0le2is012  9229  zextlt  9239  uzind2  9259  supinfneg  9489  infsupneg  9490  eluzdc  9503  qreccl  9533  elpq  9539  xltnegi  9721  xnn0lenn0nn0  9751  iccid  9811  icoshft  9876  zltaddlt1le  9893  fzofzim  10069  qbtwnxr  10139  flqeqceilz  10199  modqmuladdnn0  10249  modfzo0difsn  10276  addmodlteq  10279  frec2uzrand  10286  frecuzrdgtcl  10293  frecuzrdgfunlem  10300  facdiv  10594  facwordi  10596  faclbnd  10597  bcpasc  10622  seq3coll  10695  recvguniq  10877  abs00ap  10944  absext  10945  absnid  10955  cau3lem  10996  climuni  11172  2clim  11180  summodc  11262  fisumss  11271  fsumabs  11344  mertenslem2  11415  fprodssdc  11469  reeff1  11579  efieq1re  11650  dvdsmultr2  11708  dvdsleabs  11718  odd2np1lem  11744  odd2np1  11745  ltoddhalfle  11765  halfleoddlt  11766  m1expo  11772  nn0enne  11774  nn0ehalf  11775  nn0o1gt2  11777  flodddiv4  11806  zeqzmulgcd  11834  gcdneg  11846  gcdaddm  11848  bezoutlemaz  11867  bezoutlembz  11868  dfgcd2  11878  gcddiv  11883  dvdssqim  11888  algcvgblem  11906  algcvga  11908  lcmneg  11931  coprmgcdb  11945  coprmdvds2  11950  qredeq  11953  divgcdcoprm0  11958  divgcdcoprmex  11959  cncongr1  11960  cncongr2  11961  prmind2  11977  dvdsnprmd  11982  prmgt1  11988  nprmdvds1  11996  divgcdodd  11997  euclemma  12000  prmdvdsexpr  12004  prmfac1  12006  prmndvdsfaclt  12010  crth  12076  eulerthlemh  12083  fermltl  12086  tgtop  12428  tgidm  12434  neipsm  12514  restbasg  12528  tgrest  12529  tgcn  12568  tgcnp  12569  cnconst2  12593  cnconst  12594  cnptopresti  12598  txbasval  12627  txcnp  12631  txdis1cn  12638  bldisj  12761  xblm  12777  blssps  12787  blss  12788  blin2  12792  cnlimcim  13000  dveflem  13047  sincosq3sgn  13109  sincosq4sgn  13110  coseq0q4123  13115  ioocosf1o  13135  logbgcd1irr  13244  uzdcinzz  13332  subctctexmid  13534