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  3668  ssprsseq  3856  nlimsucg  4688  ssrelrn  4947  poltletr  5163  xp11m  5201  fvmptdf  5765  elfvmptrab1  5772  eusvobj2  6036  ovmpodf  6185  elovmporab  6254  elovmporab1w  6255  f1o2ndf1  6424  suppssdc  6460  suppssrst  6461  suppssrgst  6462  smoiso  6533  nnsseleq  6734  ecopovtrn  6866  ecopovtrng  6869  dom2lem  7011  fundmen  7047  dom1o  7069  fidifsnen  7125  findcard2  7146  findcard2s  7147  supisoex  7300  infglbti  7316  ordiso2  7326  updjud  7373  difinfsnlem  7390  enomnilem  7429  enmkvlem  7452  netap  7568  2omotaplemap  7571  cc2lem  7580  addcanpig  7649  mulcanpig  7650  addnidpig  7651  ordpipqqs  7689  ltexnqq  7723  prarloclemlo  7809  genpcdl  7834  genpcuu  7835  mulnqprl  7883  mulnqpru  7884  distrlem1prl  7897  distrlem1pru  7898  distrlem4prl  7899  distrlem4pru  7900  distrlem5prl  7901  distrlem5pru  7902  ltsopr  7911  ltexprlemfl  7924  ltexprlemfu  7926  recexprlemss1l  7950  recexprlemss1u  7951  aptiprleml  7954  ltsrprg  8062  lttrsr  8077  mulextsr1lem  8095  axapti  8344  cnegexlem1  8448  le2add  8718  lt2add  8719  ltleadd  8720  lt2sub  8734  le2sub  8735  recexre  8852  reapti  8853  apreap  8861  reapcotr  8872  remulext1  8873  apreim  8877  apcotr  8881  mulext2  8887  recexap  8927  addltmul  9475  elnnz  9587  zleloe  9624  difgtsumgt  9647  nn0n0n1ge2b  9657  nn0lt2  9659  nn0le2is012  9660  zextlt  9670  uzind2  9690  supinfneg  9927  infsupneg  9928  eluzdc  9942  qreccl  9974  elpq  9981  xltnegi  10168  xnn0lenn0nn0  10198  iccid  10258  icoshft  10323  zltaddlt1le  10341  fzofzim  10527  qbtwnxr  10617  flqeqceilz  10680  modqmuladdnn0  10730  modfzo0difsn  10757  addmodlteq  10760  frec2uzrand  10767  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  seqf1oglem1  10881  facdiv  11100  facwordi  11102  faclbnd  11103  bcpasc  11128  seq3coll  11214  fundm2domnop0  11220  fstwrdne  11263  elovmpowrd  11266  lswlgt0cl  11277  ccatrn  11297  ccatalpha  11301  swrdnd  11351  swrdswrd  11397  wrd2ind  11415  swrdccatin1  11417  pfxccatin12lem2a  11419  pfxccat3  11426  swrdccat  11427  swrdccat3blem  11431  reuccatpfxs1lem  11438  recvguniq  11680  abs00ap  11747  absext  11748  absnid  11758  cau3lem  11799  climuni  11978  2clim  11986  summodc  12069  fisumss  12078  fsumabs  12151  mertenslem2  12222  fprodssdc  12276  reeff1  12386  efieq1re  12458  dvdsmultr2  12519  dvdsleabs  12531  odd2np1lem  12558  odd2np1  12559  ltoddhalfle  12579  halfleoddlt  12580  m1expo  12586  nn0enne  12588  nn0ehalf  12589  nn0o1gt2  12591  flodddiv4  12622  zeqzmulgcd  12666  gcdneg  12678  gcdaddm  12680  bezoutlemaz  12699  bezoutlembz  12700  dfgcd2  12710  gcddiv  12715  dvdssqim  12720  algcvgblem  12746  algcvga  12748  lcmneg  12771  coprmgcdb  12785  coprmdvds2  12790  qredeq  12793  divgcdcoprm0  12798  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  prmind2  12817  dvdsnprmd  12822  prmgt1  12829  nprmdvds1  12837  divgcdodd  12840  euclemma  12843  prmdvdsexpr  12847  prmfac1  12849  prmndvdsfaclt  12853  crth  12921  eulerthlemh  12928  fermltl  12931  nnnn0modprm0  12953  coprimeprodsq2  12956  pythagtriplem2  12964  pcpremul  12991  pcdvdsb  13018  pc2dvds  13028  pc11  13029  dvdsprmpweqnn  13034  dvdsprmpweqle  13035  difsqpwdvds  13036  pcfac  13048  oddprmdvds  13052  prmpwdvds  13053  1arith  13065  4sqlem11  13099  4sqlem12  13100  imasaddfnlemg  13527  erlecpbl  13545  xpsff1o  13562  imasmnd2  13665  grp1inv  13820  imasgrp2  13827  ghmpreima  13983  imasabl  14053  imasrng  14100  imasring  14208  dvdsrtr  14246  dvdsrmul1  14247  unitgrp  14261  znidomb  14806  tgtop  14933  tgidm  14939  neipsm  15019  restbasg  15033  tgrest  15034  tgcn  15073  tgcnp  15074  cnconst2  15098  cnconst  15099  cnptopresti  15103  txbasval  15132  txcnp  15136  txdis1cn  15143  bldisj  15266  xblm  15282  blssps  15292  blss  15293  blin2  15297  cnlimcim  15536  dveflem  15591  sincosq3sgn  15693  sincosq4sgn  15694  coseq0q4123  15699  ioocosf1o  15719  logbgcd1irr  15832  pellexlem1  15845  pellexlem3  15847  mpodvdsmulf1o  15858  zabsle1  15872  lgsdir2lem5  15905  lgsne0  15911  lgsdirnn0  15920  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem2  15944  lgsquadlem1  15950  2lgslem1a1  15959  2lgslem1b  15962  2lgslem1c  15963  2lgs  15977  2lgsoddprmlem2  15979  upgrpredgv  16141  ausgrumgrien  16165  ausgrusgrien  16166  usgruspgrben  16181  uhgr2edg  16201  usgredg4  16210  ushgredgedg  16221  ushgredgedgloop  16223  edg0usgr  16242  uhgrspansubgrlem  16271  wlkl1loop  16353  wlk1walkdom  16354  wlklenvclwlk  16368  wlkres  16374  clwwlknonex2  16434  uzdcinzz  16570  subctctexmid  16774