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  4563  poltletr  5026  xp11m  5064  fvmptdf  5600  elfvmptrab1  5607  eusvobj2  5856  ovmpodf  6001  f1o2ndf1  6224  smoiso  6298  nnsseleq  6497  ecopovtrn  6627  ecopovtrng  6630  dom2lem  6767  fundmen  6801  fidifsnen  6865  findcard2  6884  findcard2s  6885  supisoex  7003  infglbti  7019  ordiso2  7029  updjud  7076  difinfsnlem  7093  enomnilem  7131  enmkvlem  7154  netap  7248  2omotaplemap  7251  cc2lem  7260  addcanpig  7328  mulcanpig  7329  addnidpig  7330  ordpipqqs  7368  ltexnqq  7402  prarloclemlo  7488  genpcdl  7513  genpcuu  7514  mulnqprl  7562  mulnqpru  7563  distrlem1prl  7576  distrlem1pru  7577  distrlem4prl  7578  distrlem4pru  7579  distrlem5prl  7580  distrlem5pru  7581  ltsopr  7590  ltexprlemfl  7603  ltexprlemfu  7605  recexprlemss1l  7629  recexprlemss1u  7630  aptiprleml  7633  ltsrprg  7741  lttrsr  7756  mulextsr1lem  7774  axapti  8022  cnegexlem1  8126  le2add  8395  lt2add  8396  ltleadd  8397  lt2sub  8411  le2sub  8412  recexre  8529  reapti  8530  apreap  8538  reapcotr  8549  remulext1  8550  apreim  8554  apcotr  8558  mulext2  8564  recexap  8604  addltmul  9149  elnnz  9257  zleloe  9294  difgtsumgt  9316  nn0n0n1ge2b  9326  nn0lt2  9328  nn0le2is012  9329  zextlt  9339  uzind2  9359  supinfneg  9589  infsupneg  9590  eluzdc  9604  qreccl  9636  elpq  9642  xltnegi  9829  xnn0lenn0nn0  9859  iccid  9919  icoshft  9984  zltaddlt1le  10001  fzofzim  10181  qbtwnxr  10251  flqeqceilz  10311  modqmuladdnn0  10361  modfzo0difsn  10388  addmodlteq  10391  frec2uzrand  10398  frecuzrdgtcl  10405  frecuzrdgfunlem  10412  facdiv  10709  facwordi  10711  faclbnd  10712  bcpasc  10737  seq3coll  10813  recvguniq  10995  abs00ap  11062  absext  11063  absnid  11073  cau3lem  11114  climuni  11292  2clim  11300  summodc  11382  fisumss  11391  fsumabs  11464  mertenslem2  11535  fprodssdc  11589  reeff1  11699  efieq1re  11770  dvdsmultr2  11831  dvdsleabs  11841  odd2np1lem  11867  odd2np1  11868  ltoddhalfle  11888  halfleoddlt  11889  m1expo  11895  nn0enne  11897  nn0ehalf  11898  nn0o1gt2  11900  flodddiv4  11929  zeqzmulgcd  11961  gcdneg  11973  gcdaddm  11975  bezoutlemaz  11994  bezoutlembz  11995  dfgcd2  12005  gcddiv  12010  dvdssqim  12015  algcvgblem  12039  algcvga  12041  lcmneg  12064  coprmgcdb  12078  coprmdvds2  12083  qredeq  12086  divgcdcoprm0  12091  divgcdcoprmex  12092  cncongr1  12093  cncongr2  12094  prmind2  12110  dvdsnprmd  12115  prmgt1  12122  nprmdvds1  12130  divgcdodd  12133  euclemma  12136  prmdvdsexpr  12140  prmfac1  12142  prmndvdsfaclt  12146  crth  12214  eulerthlemh  12221  fermltl  12224  nnnn0modprm0  12245  coprimeprodsq2  12248  pythagtriplem2  12256  pcpremul  12283  pcdvdsb  12309  pc2dvds  12319  pc11  12320  dvdsprmpweqnn  12325  dvdsprmpweqle  12326  difsqpwdvds  12327  pcfac  12338  oddprmdvds  12342  prmpwdvds  12343  1arith  12355  grp1inv  12905  dvdsrtr  13169  dvdsrmul1  13170  unitgrp  13184  tgtop  13350  tgidm  13356  neipsm  13436  restbasg  13450  tgrest  13451  tgcn  13490  tgcnp  13491  cnconst2  13515  cnconst  13516  cnptopresti  13520  txbasval  13549  txcnp  13553  txdis1cn  13560  bldisj  13683  xblm  13699  blssps  13709  blss  13710  blin2  13714  cnlimcim  13922  dveflem  13969  sincosq3sgn  14031  sincosq4sgn  14032  coseq0q4123  14037  ioocosf1o  14057  logbgcd1irr  14167  zabsle1  14182  lgsdir2lem5  14215  lgsne0  14221  lgsdirnn0  14230  uzdcinzz  14321  subctctexmid  14521