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  3651  ssprsseq  3835  nlimsucg  4664  ssrelrn  4922  poltletr  5137  xp11m  5175  fvmptdf  5734  elfvmptrab1  5741  eusvobj2  6004  ovmpodf  6153  elovmporab  6222  elovmporab1w  6223  f1o2ndf1  6393  smoiso  6468  nnsseleq  6669  ecopovtrn  6801  ecopovtrng  6804  dom2lem  6945  fundmen  6981  dom1o  7002  fidifsnen  7057  findcard2  7078  findcard2s  7079  supisoex  7208  infglbti  7224  ordiso2  7234  updjud  7281  difinfsnlem  7298  enomnilem  7337  enmkvlem  7360  netap  7473  2omotaplemap  7476  cc2lem  7485  addcanpig  7554  mulcanpig  7555  addnidpig  7556  ordpipqqs  7594  ltexnqq  7628  prarloclemlo  7714  genpcdl  7739  genpcuu  7740  mulnqprl  7788  mulnqpru  7789  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  distrlem5prl  7806  distrlem5pru  7807  ltsopr  7816  ltexprlemfl  7829  ltexprlemfu  7831  recexprlemss1l  7855  recexprlemss1u  7856  aptiprleml  7859  ltsrprg  7967  lttrsr  7982  mulextsr1lem  8000  axapti  8250  cnegexlem1  8354  le2add  8624  lt2add  8625  ltleadd  8626  lt2sub  8640  le2sub  8641  recexre  8758  reapti  8759  apreap  8767  reapcotr  8778  remulext1  8779  apreim  8783  apcotr  8787  mulext2  8793  recexap  8833  addltmul  9381  elnnz  9489  zleloe  9526  difgtsumgt  9549  nn0n0n1ge2b  9559  nn0lt2  9561  nn0le2is012  9562  zextlt  9572  uzind2  9592  supinfneg  9829  infsupneg  9830  eluzdc  9844  qreccl  9876  elpq  9883  xltnegi  10070  xnn0lenn0nn0  10100  iccid  10160  icoshft  10225  zltaddlt1le  10242  fzofzim  10428  qbtwnxr  10518  flqeqceilz  10581  modqmuladdnn0  10631  modfzo0difsn  10658  addmodlteq  10661  frec2uzrand  10668  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1oglem1  10782  facdiv  11001  facwordi  11003  faclbnd  11004  bcpasc  11029  seq3coll  11107  fundm2domnop0  11113  fstwrdne  11156  elovmpowrd  11159  lswlgt0cl  11170  ccatrn  11190  ccatalpha  11194  swrdnd  11244  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem2a  11312  pfxccat3  11319  swrdccat  11320  swrdccat3blem  11324  reuccatpfxs1lem  11331  recvguniq  11560  abs00ap  11627  absext  11628  absnid  11638  cau3lem  11679  climuni  11858  2clim  11866  summodc  11949  fisumss  11958  fsumabs  12031  mertenslem2  12102  fprodssdc  12156  reeff1  12266  efieq1re  12338  dvdsmultr2  12399  dvdsleabs  12411  odd2np1lem  12438  odd2np1  12439  ltoddhalfle  12459  halfleoddlt  12460  m1expo  12466  nn0enne  12468  nn0ehalf  12469  nn0o1gt2  12471  flodddiv4  12502  zeqzmulgcd  12546  gcdneg  12558  gcdaddm  12560  bezoutlemaz  12579  bezoutlembz  12580  dfgcd2  12590  gcddiv  12595  dvdssqim  12600  algcvgblem  12626  algcvga  12628  lcmneg  12651  coprmgcdb  12665  coprmdvds2  12670  qredeq  12673  divgcdcoprm0  12678  divgcdcoprmex  12679  cncongr1  12680  cncongr2  12681  prmind2  12697  dvdsnprmd  12702  prmgt1  12709  nprmdvds1  12717  divgcdodd  12720  euclemma  12723  prmdvdsexpr  12727  prmfac1  12729  prmndvdsfaclt  12733  crth  12801  eulerthlemh  12808  fermltl  12811  nnnn0modprm0  12833  coprimeprodsq2  12836  pythagtriplem2  12844  pcpremul  12871  pcdvdsb  12898  pc2dvds  12908  pc11  12909  dvdsprmpweqnn  12914  dvdsprmpweqle  12915  difsqpwdvds  12916  pcfac  12928  oddprmdvds  12932  prmpwdvds  12933  1arith  12945  4sqlem11  12979  4sqlem12  12980  imasaddfnlemg  13402  erlecpbl  13420  xpsff1o  13437  imasmnd2  13540  grp1inv  13695  imasgrp2  13702  ghmpreima  13858  imasabl  13928  imasrng  13975  imasring  14083  dvdsrtr  14121  dvdsrmul1  14122  unitgrp  14136  znidomb  14678  tgtop  14798  tgidm  14804  neipsm  14884  restbasg  14898  tgrest  14899  tgcn  14938  tgcnp  14939  cnconst2  14963  cnconst  14964  cnptopresti  14968  txbasval  14997  txcnp  15001  txdis1cn  15008  bldisj  15131  xblm  15147  blssps  15157  blss  15158  blin2  15162  cnlimcim  15401  dveflem  15456  sincosq3sgn  15558  sincosq4sgn  15559  coseq0q4123  15564  ioocosf1o  15584  logbgcd1irr  15697  mpodvdsmulf1o  15720  zabsle1  15734  lgsdir2lem5  15767  lgsne0  15773  lgsdirnn0  15782  gausslemma2dlem0i  15792  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  gausslemma2dlem7  15803  gausslemma2d  15804  lgseisenlem2  15806  lgsquadlem1  15812  2lgslem1a1  15821  2lgslem1b  15824  2lgslem1c  15825  2lgs  15839  2lgsoddprmlem2  15841  upgrpredgv  16003  ausgrumgrien  16027  ausgrusgrien  16028  usgruspgrben  16043  uhgr2edg  16063  usgredg4  16072  ushgredgedg  16083  ushgredgedgloop  16085  edg0usgr  16104  uhgrspansubgrlem  16133  wlkl1loop  16215  wlk1walkdom  16216  wlklenvclwlk  16230  wlkres  16236  clwwlknonex2  16296  uzdcinzz  16420  subctctexmid  16627