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  nlimsucg  4567  poltletr  5031  xp11m  5069  fvmptdf  5605  elfvmptrab1  5612  eusvobj2  5863  ovmpodf  6008  f1o2ndf1  6231  smoiso  6305  nnsseleq  6504  ecopovtrn  6634  ecopovtrng  6637  dom2lem  6774  fundmen  6808  fidifsnen  6872  findcard2  6891  findcard2s  6892  supisoex  7010  infglbti  7026  ordiso2  7036  updjud  7083  difinfsnlem  7100  enomnilem  7138  enmkvlem  7161  netap  7255  2omotaplemap  7258  cc2lem  7267  addcanpig  7335  mulcanpig  7336  addnidpig  7337  ordpipqqs  7375  ltexnqq  7409  prarloclemlo  7495  genpcdl  7520  genpcuu  7521  mulnqprl  7569  mulnqpru  7570  distrlem1prl  7583  distrlem1pru  7584  distrlem4prl  7585  distrlem4pru  7586  distrlem5prl  7587  distrlem5pru  7588  ltsopr  7597  ltexprlemfl  7610  ltexprlemfu  7612  recexprlemss1l  7636  recexprlemss1u  7637  aptiprleml  7640  ltsrprg  7748  lttrsr  7763  mulextsr1lem  7781  axapti  8030  cnegexlem1  8134  le2add  8403  lt2add  8404  ltleadd  8405  lt2sub  8419  le2sub  8420  recexre  8537  reapti  8538  apreap  8546  reapcotr  8557  remulext1  8558  apreim  8562  apcotr  8566  mulext2  8572  recexap  8612  addltmul  9157  elnnz  9265  zleloe  9302  difgtsumgt  9324  nn0n0n1ge2b  9334  nn0lt2  9336  nn0le2is012  9337  zextlt  9347  uzind2  9367  supinfneg  9597  infsupneg  9598  eluzdc  9612  qreccl  9644  elpq  9650  xltnegi  9837  xnn0lenn0nn0  9867  iccid  9927  icoshft  9992  zltaddlt1le  10009  fzofzim  10190  qbtwnxr  10260  flqeqceilz  10320  modqmuladdnn0  10370  modfzo0difsn  10397  addmodlteq  10400  frec2uzrand  10407  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  facdiv  10720  facwordi  10722  faclbnd  10723  bcpasc  10748  seq3coll  10824  recvguniq  11006  abs00ap  11073  absext  11074  absnid  11084  cau3lem  11125  climuni  11303  2clim  11311  summodc  11393  fisumss  11402  fsumabs  11475  mertenslem2  11546  fprodssdc  11600  reeff1  11710  efieq1re  11781  dvdsmultr2  11842  dvdsleabs  11853  odd2np1lem  11879  odd2np1  11880  ltoddhalfle  11900  halfleoddlt  11901  m1expo  11907  nn0enne  11909  nn0ehalf  11910  nn0o1gt2  11912  flodddiv4  11941  zeqzmulgcd  11973  gcdneg  11985  gcdaddm  11987  bezoutlemaz  12006  bezoutlembz  12007  dfgcd2  12017  gcddiv  12022  dvdssqim  12027  algcvgblem  12051  algcvga  12053  lcmneg  12076  coprmgcdb  12090  coprmdvds2  12095  qredeq  12098  divgcdcoprm0  12103  divgcdcoprmex  12104  cncongr1  12105  cncongr2  12106  prmind2  12122  dvdsnprmd  12127  prmgt1  12134  nprmdvds1  12142  divgcdodd  12145  euclemma  12148  prmdvdsexpr  12152  prmfac1  12154  prmndvdsfaclt  12158  crth  12226  eulerthlemh  12233  fermltl  12236  nnnn0modprm0  12257  coprimeprodsq2  12260  pythagtriplem2  12268  pcpremul  12295  pcdvdsb  12321  pc2dvds  12331  pc11  12332  dvdsprmpweqnn  12337  dvdsprmpweqle  12338  difsqpwdvds  12339  pcfac  12350  oddprmdvds  12354  prmpwdvds  12355  1arith  12367  imasaddfnlemg  12740  erlecpbl  12756  xpsff1o  12773  grp1inv  12982  dvdsrtr  13275  dvdsrmul1  13276  unitgrp  13290  tgtop  13607  tgidm  13613  neipsm  13693  restbasg  13707  tgrest  13708  tgcn  13747  tgcnp  13748  cnconst2  13772  cnconst  13773  cnptopresti  13777  txbasval  13806  txcnp  13810  txdis1cn  13817  bldisj  13940  xblm  13956  blssps  13966  blss  13967  blin2  13971  cnlimcim  14179  dveflem  14226  sincosq3sgn  14288  sincosq4sgn  14289  coseq0q4123  14294  ioocosf1o  14314  logbgcd1irr  14424  zabsle1  14439  lgsdir2lem5  14472  lgsne0  14478  lgsdirnn0  14487  lgseisenlem2  14490  2lgsoddprmlem2  14493  uzdcinzz  14589  subctctexmid  14789