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  7337  2omotaplemap  7340  cc2lem  7349  addcanpig  7418  mulcanpig  7419  addnidpig  7420  ordpipqqs  7458  ltexnqq  7492  prarloclemlo  7578  genpcdl  7603  genpcuu  7604  mulnqprl  7652  mulnqpru  7653  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  distrlem5prl  7670  distrlem5pru  7671  ltsopr  7680  ltexprlemfl  7693  ltexprlemfu  7695  recexprlemss1l  7719  recexprlemss1u  7720  aptiprleml  7723  ltsrprg  7831  lttrsr  7846  mulextsr1lem  7864  axapti  8114  cnegexlem1  8218  le2add  8488  lt2add  8489  ltleadd  8490  lt2sub  8504  le2sub  8505  recexre  8622  reapti  8623  apreap  8631  reapcotr  8642  remulext1  8643  apreim  8647  apcotr  8651  mulext2  8657  recexap  8697  addltmul  9245  elnnz  9353  zleloe  9390  difgtsumgt  9412  nn0n0n1ge2b  9422  nn0lt2  9424  nn0le2is012  9425  zextlt  9435  uzind2  9455  supinfneg  9686  infsupneg  9687  eluzdc  9701  qreccl  9733  elpq  9740  xltnegi  9927  xnn0lenn0nn0  9957  iccid  10017  icoshft  10082  zltaddlt1le  10099  fzofzim  10281  qbtwnxr  10364  flqeqceilz  10427  modqmuladdnn0  10477  modfzo0difsn  10504  addmodlteq  10507  frec2uzrand  10514  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  seqf1oglem1  10628  facdiv  10847  facwordi  10849  faclbnd  10850  bcpasc  10875  seq3coll  10951  fstwrdne  10990  elovmpowrd  10993  recvguniq  11177  abs00ap  11244  absext  11245  absnid  11255  cau3lem  11296  climuni  11475  2clim  11483  summodc  11565  fisumss  11574  fsumabs  11647  mertenslem2  11718  fprodssdc  11772  reeff1  11882  efieq1re  11954  dvdsmultr2  12015  dvdsleabs  12027  odd2np1lem  12054  odd2np1  12055  ltoddhalfle  12075  halfleoddlt  12076  m1expo  12082  nn0enne  12084  nn0ehalf  12085  nn0o1gt2  12087  flodddiv4  12118  zeqzmulgcd  12162  gcdneg  12174  gcdaddm  12176  bezoutlemaz  12195  bezoutlembz  12196  dfgcd2  12206  gcddiv  12211  dvdssqim  12216  algcvgblem  12242  algcvga  12244  lcmneg  12267  coprmgcdb  12281  coprmdvds2  12286  qredeq  12289  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  prmind2  12313  dvdsnprmd  12318  prmgt1  12325  nprmdvds1  12333  divgcdodd  12336  euclemma  12339  prmdvdsexpr  12343  prmfac1  12345  prmndvdsfaclt  12349  crth  12417  eulerthlemh  12424  fermltl  12427  nnnn0modprm0  12449  coprimeprodsq2  12452  pythagtriplem2  12460  pcpremul  12487  pcdvdsb  12514  pc2dvds  12524  pc11  12525  dvdsprmpweqnn  12530  dvdsprmpweqle  12531  difsqpwdvds  12532  pcfac  12544  oddprmdvds  12548  prmpwdvds  12549  1arith  12561  4sqlem11  12595  4sqlem12  12596  imasaddfnlemg  13016  erlecpbl  13034  xpsff1o  13051  imasmnd2  13154  grp1inv  13309  imasgrp2  13316  ghmpreima  13472  imasabl  13542  imasrng  13588  imasring  13696  dvdsrtr  13733  dvdsrmul1  13734  unitgrp  13748  znidomb  14290  tgtop  14388  tgidm  14394  neipsm  14474  restbasg  14488  tgrest  14489  tgcn  14528  tgcnp  14529  cnconst2  14553  cnconst  14554  cnptopresti  14558  txbasval  14587  txcnp  14591  txdis1cn  14598  bldisj  14721  xblm  14737  blssps  14747  blss  14748  blin2  14752  cnlimcim  14991  dveflem  15046  sincosq3sgn  15148  sincosq4sgn  15149  coseq0q4123  15154  ioocosf1o  15174  logbgcd1irr  15287  mpodvdsmulf1o  15310  zabsle1  15324  lgsdir2lem5  15357  lgsne0  15363  lgsdirnn0  15372  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem7  15393  gausslemma2d  15394  lgseisenlem2  15396  lgsquadlem1  15402  2lgslem1a1  15411  2lgslem1b  15414  2lgslem1c  15415  2lgs  15429  2lgsoddprmlem2  15431  uzdcinzz  15528  subctctexmid  15731