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  3672  ssprsseq  3861  nlimsucg  4693  ssrelrn  4952  poltletr  5168  xp11m  5206  fvmptdf  5770  elfvmptrab1  5777  eusvobj2  6044  ovmpodf  6193  elovmporab  6262  elovmporab1w  6263  f1o2ndf1  6437  suppssdc  6473  suppssrst  6474  suppssrgst  6475  smoiso  6546  nnsseleq  6747  ecopovtrn  6879  ecopovtrng  6882  dom2lem  7024  fundmen  7060  dom1o  7082  fidifsnen  7138  findcard2  7159  findcard2s  7160  supisoex  7313  infglbti  7329  ordiso2  7339  updjud  7386  difinfsnlem  7403  enomnilem  7442  enmkvlem  7465  netap  7584  2omotaplemap  7587  cc2lem  7596  addcanpig  7665  mulcanpig  7666  addnidpig  7667  ordpipqqs  7705  ltexnqq  7739  prarloclemlo  7825  genpcdl  7850  genpcuu  7851  mulnqprl  7899  mulnqpru  7900  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  distrlem5prl  7917  distrlem5pru  7918  ltsopr  7927  ltexprlemfl  7940  ltexprlemfu  7942  recexprlemss1l  7966  recexprlemss1u  7967  aptiprleml  7970  ltsrprg  8078  lttrsr  8093  mulextsr1lem  8111  axapti  8360  cnegexlem1  8464  le2add  8735  lt2add  8736  ltleadd  8737  lt2sub  8751  le2sub  8752  recexre  8869  reapti  8870  apreap  8878  reapcotr  8889  remulext1  8890  apreim  8894  apcotr  8898  mulext2  8904  recexap  8944  addltmul  9492  elnnz  9604  zleloe  9641  difgtsumgt  9664  nn0n0n1ge2b  9675  nn0lt2  9677  nn0le2is012  9678  zextlt  9688  uzind2  9708  supinfneg  9945  infsupneg  9946  eluzdc  9960  qreccl  9992  elpq  9999  xltnegi  10187  xnn0lenn0nn0  10217  iccid  10277  icoshft  10342  zltaddlt1le  10360  fzofzim  10549  qbtwnxr  10641  flqeqceilz  10704  modqmuladdnn0  10754  modfzo0difsn  10781  addmodlteq  10784  frec2uzrand  10791  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqf1oglem1  10905  facdiv  11125  facwordi  11127  faclbnd  11128  bcpasc  11153  seq3coll  11239  fundm2domnop0  11245  fstwrdne  11288  elovmpowrd  11291  lswlgt0cl  11302  ccatrn  11322  ccatalpha  11326  swrdnd  11376  swrdswrd  11422  wrd2ind  11440  swrdccatin1  11442  pfxccatin12lem2a  11444  pfxccat3  11451  swrdccat  11452  swrdccat3blem  11456  reuccatpfxs1lem  11463  recvguniq  11705  abs00ap  11772  absext  11773  absnid  11783  cau3lem  11824  climuni  12003  2clim  12011  summodc  12094  fisumss  12103  fsumabs  12176  mertenslem2  12247  fprodssdc  12301  reeff1  12411  efieq1re  12483  dvdsmultr2  12544  dvdsleabs  12556  odd2np1lem  12583  odd2np1  12584  ltoddhalfle  12604  halfleoddlt  12605  m1expo  12611  nn0enne  12613  nn0ehalf  12614  nn0o1gt2  12616  flodddiv4  12647  zeqzmulgcd  12691  gcdneg  12703  gcdaddm  12705  bezoutlemaz  12724  bezoutlembz  12725  dfgcd2  12735  gcddiv  12740  dvdssqim  12745  algcvgblem  12771  algcvga  12773  lcmneg  12796  coprmgcdb  12810  coprmdvds2  12815  qredeq  12818  divgcdcoprm0  12823  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  prmind2  12842  dvdsnprmd  12847  prmgt1  12854  nprmdvds1  12862  divgcdodd  12865  euclemma  12868  prmdvdsexpr  12872  prmfac1  12874  prmndvdsfaclt  12878  crth  12946  eulerthlemh  12953  fermltl  12956  nnnn0modprm0  12978  coprimeprodsq2  12981  pythagtriplem2  12989  pcpremul  13016  pcdvdsb  13043  pc2dvds  13053  pc11  13054  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  difsqpwdvds  13061  pcfac  13073  oddprmdvds  13077  prmpwdvds  13078  1arith  13090  4sqlem11  13124  4sqlem12  13125  ballotfilemfrceq  13216  imasaddfnlemg  13578  erlecpbl  13596  xpsff1o  13613  imasmnd2  13707  grp1inv  13862  imasgrp2  13863  ghmpreima  14019  imasabl  14089  imasrng  14195  imasring  14307  dvdsrtr  14346  dvdsrmul1  14347  unitgrp  14361  znidomb  14932  tgtop  15059  tgidm  15065  neipsm  15145  restbasg  15159  tgrest  15160  tgcn  15199  tgcnp  15200  cnconst2  15224  cnconst  15225  cnptopresti  15229  txbasval  15258  txcnp  15262  txdis1cn  15269  bldisj  15392  xblm  15408  blssps  15418  blss  15419  blin2  15423  cnlimcim  15662  dveflem  15717  sincosq3sgn  15819  sincosq4sgn  15820  coseq0q4123  15825  ioocosf1o  15845  logbgcd1irr  15958  pellexlem1  15971  pellexlem3  15973  mpodvdsmulf1o  15984  zabsle1  15998  lgsdir2lem5  16031  lgsne0  16037  lgsdirnn0  16046  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem2  16070  lgsquadlem1  16076  2lgslem1a1  16085  2lgslem1b  16088  2lgslem1c  16089  2lgs  16103  2lgsoddprmlem2  16105  upgrpredgv  16267  ausgrumgrien  16291  ausgrusgrien  16292  usgruspgrben  16307  uhgr2edg  16327  usgredg4  16336  ushgredgedg  16347  ushgredgedgloop  16349  edg0usgr  16368  uhgrspansubgrlem  16397  wlkl1loop  16479  wlk1walkdom  16480  wlklenvclwlk  16494  wlkres  16500  clwwlknonex2  16560  uzdcinzz  16696  subctctexmid  16900