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  3605  nlimsucg  4603  poltletr  5071  xp11m  5109  fvmptdf  5652  elfvmptrab1  5659  eusvobj2  5911  ovmpodf  6058  elovmporab  6127  elovmporab1w  6128  f1o2ndf1  6295  smoiso  6369  nnsseleq  6568  ecopovtrn  6700  ecopovtrng  6703  dom2lem  6840  fundmen  6874  fidifsnen  6940  findcard2  6959  findcard2s  6960  supisoex  7084  infglbti  7100  ordiso2  7110  updjud  7157  difinfsnlem  7174  enomnilem  7213  enmkvlem  7236  netap  7339  2omotaplemap  7342  cc2lem  7351  addcanpig  7420  mulcanpig  7421  addnidpig  7422  ordpipqqs  7460  ltexnqq  7494  prarloclemlo  7580  genpcdl  7605  genpcuu  7606  mulnqprl  7654  mulnqpru  7655  distrlem1prl  7668  distrlem1pru  7669  distrlem4prl  7670  distrlem4pru  7671  distrlem5prl  7672  distrlem5pru  7673  ltsopr  7682  ltexprlemfl  7695  ltexprlemfu  7697  recexprlemss1l  7721  recexprlemss1u  7722  aptiprleml  7725  ltsrprg  7833  lttrsr  7848  mulextsr1lem  7866  axapti  8116  cnegexlem1  8220  le2add  8490  lt2add  8491  ltleadd  8492  lt2sub  8506  le2sub  8507  recexre  8624  reapti  8625  apreap  8633  reapcotr  8644  remulext1  8645  apreim  8649  apcotr  8653  mulext2  8659  recexap  8699  addltmul  9247  elnnz  9355  zleloe  9392  difgtsumgt  9414  nn0n0n1ge2b  9424  nn0lt2  9426  nn0le2is012  9427  zextlt  9437  uzind2  9457  supinfneg  9688  infsupneg  9689  eluzdc  9703  qreccl  9735  elpq  9742  xltnegi  9929  xnn0lenn0nn0  9959  iccid  10019  icoshft  10084  zltaddlt1le  10101  fzofzim  10283  qbtwnxr  10366  flqeqceilz  10429  modqmuladdnn0  10479  modfzo0difsn  10506  addmodlteq  10509  frec2uzrand  10516  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  seqf1oglem1  10630  facdiv  10849  facwordi  10851  faclbnd  10852  bcpasc  10877  seq3coll  10953  fstwrdne  10992  elovmpowrd  10995  recvguniq  11179  abs00ap  11246  absext  11247  absnid  11257  cau3lem  11298  climuni  11477  2clim  11485  summodc  11567  fisumss  11576  fsumabs  11649  mertenslem2  11720  fprodssdc  11774  reeff1  11884  efieq1re  11956  dvdsmultr2  12017  dvdsleabs  12029  odd2np1lem  12056  odd2np1  12057  ltoddhalfle  12077  halfleoddlt  12078  m1expo  12084  nn0enne  12086  nn0ehalf  12087  nn0o1gt2  12089  flodddiv4  12120  zeqzmulgcd  12164  gcdneg  12176  gcdaddm  12178  bezoutlemaz  12197  bezoutlembz  12198  dfgcd2  12208  gcddiv  12213  dvdssqim  12218  algcvgblem  12244  algcvga  12246  lcmneg  12269  coprmgcdb  12283  coprmdvds2  12288  qredeq  12291  divgcdcoprm0  12296  divgcdcoprmex  12297  cncongr1  12298  cncongr2  12299  prmind2  12315  dvdsnprmd  12320  prmgt1  12327  nprmdvds1  12335  divgcdodd  12338  euclemma  12341  prmdvdsexpr  12345  prmfac1  12347  prmndvdsfaclt  12351  crth  12419  eulerthlemh  12426  fermltl  12429  nnnn0modprm0  12451  coprimeprodsq2  12454  pythagtriplem2  12462  pcpremul  12489  pcdvdsb  12516  pc2dvds  12526  pc11  12527  dvdsprmpweqnn  12532  dvdsprmpweqle  12533  difsqpwdvds  12534  pcfac  12546  oddprmdvds  12550  prmpwdvds  12551  1arith  12563  4sqlem11  12597  4sqlem12  12598  imasaddfnlemg  13018  erlecpbl  13036  xpsff1o  13053  imasmnd2  13156  grp1inv  13311  imasgrp2  13318  ghmpreima  13474  imasabl  13544  imasrng  13590  imasring  13698  dvdsrtr  13735  dvdsrmul1  13736  unitgrp  13750  znidomb  14292  tgtop  14412  tgidm  14418  neipsm  14498  restbasg  14512  tgrest  14513  tgcn  14552  tgcnp  14553  cnconst2  14577  cnconst  14578  cnptopresti  14582  txbasval  14611  txcnp  14615  txdis1cn  14622  bldisj  14745  xblm  14761  blssps  14771  blss  14772  blin2  14776  cnlimcim  15015  dveflem  15070  sincosq3sgn  15172  sincosq4sgn  15173  coseq0q4123  15178  ioocosf1o  15198  logbgcd1irr  15311  mpodvdsmulf1o  15334  zabsle1  15348  lgsdir2lem5  15381  lgsne0  15387  lgsdirnn0  15396  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  gausslemma2dlem2  15411  gausslemma2dlem7  15417  gausslemma2d  15418  lgseisenlem2  15420  lgsquadlem1  15426  2lgslem1a1  15435  2lgslem1b  15438  2lgslem1c  15439  2lgs  15453  2lgsoddprmlem2  15455  uzdcinzz  15552  subctctexmid  15755