Theorem sylbid 150

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbid.1	|- ( ph -> ( ps <-> ch ) )
sylbid.2	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
sylbid	|- ( ph -> ( ps -> th ) )

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	biimpd 144	. 2 |- ( ph -> ( ps -> ch ) )
3		sylbid.2	. 2 |- ( ph -> ( ch -> th ) )
4	2, 3	syld 45	1 |- ( ph -> ( ps -> th ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  ifnebibdc  3686  ssprsseq  3877  nlimsucg  4715  ssrelrn  4974  poltletr  5191  xp11m  5229  fvmptdf  5796  elfvmptrab1  5804  eusvobj2  6074  ovmpodf  6223  elovmporab  6292  elovmporab1w  6293  f1o2ndf1  6468  suppssdc  6504  suppssrst  6505  suppssrgst  6506  smoiso  6577  nnsseleq  6778  ecopovtrn  6910  ecopovtrng  6913  dom2lem  7062  fundmen  7098  dom1o  7120  fidifsnen  7176  findcard2  7197  findcard2s  7198  supisoex  7355  infglbti  7371  ordiso2  7381  updjud  7428  difinfsnlem  7445  enomnilem  7484  enmkvlem  7507  netap  7626  2omotaplemap  7629  cc2lem  7638  addcanpig  7707  mulcanpig  7708  addnidpig  7709  ordpipqqs  7747  ltexnqq  7781  prarloclemlo  7867  genpcdl  7892  genpcuu  7893  mulnqprl  7941  mulnqpru  7942  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  distrlem5prl  7959  distrlem5pru  7960  ltsopr  7969  ltexprlemfl  7982  ltexprlemfu  7984  recexprlemss1l  8008  recexprlemss1u  8009  aptiprleml  8012  ltsrprg  8120  lttrsr  8135  mulextsr1lem  8153  axapti  8402  cnegexlem1  8508  le2add  8779  lt2add  8780  ltleadd  8781  lt2sub  8795  le2sub  8796  recexre  8914  reapti  8915  apreap  8923  reapcotr  8934  remulext1  8935  apreim  8939  apcotr  8943  mulext2  8949  recexap  8989  addltmul  9553  elnnz  9665  zleloe  9702  difgtsumgt  9725  nn0n0n1ge2b  9736  nn0lt2  9738  nn0le2is012  9739  zextlt  9749  uzind2  9769  supinfneg  10011  infsupneg  10012  eluzdc  10026  qreccl  10058  elpq  10066  xltnegi  10254  xnn0lenn0nn0  10284  iccid  10344  icoshft  10409  zltaddlt1le  10427  fzofzim  10617  qbtwnxr  10709  flqeqceilz  10776  modqmuladdnn0  10826  modfzo0difsn  10853  addmodlteq  10856  frec2uzrand  10863  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqf1oglem1  10977  facdiv  11198  facwordi  11200  faclbnd  11201  bcpasc  11226  seq3coll  11316  fundm2domnop0  11322  fstwrdne  11365  elovmpowrd  11368  lswlgt0cl  11379  ccatrn  11399  ccatalpha  11403  swrdnd  11453  swrdswrd  11499  wrd2ind  11517  swrdccatin1  11519  pfxccatin12lem2a  11521  pfxccat3  11528  swrdccat  11529  swrdccat3blem  11533  reuccatpfxs1lem  11540  recvguniq  11783  abs00ap  11850  absext  11851  absnid  11861  cau3lem  11903  climuni  12084  2clim  12092  summodc  12175  fisumss  12184  fsumabs  12257  mertenslem2  12328  fprodssdc  12382  reeff1  12492  efieq1re  12564  dvdsmultr2  12625  dvdsleabs  12637  odd2np1lem  12664  odd2np1  12665  ltoddhalfle  12685  halfleoddlt  12686  m1expo  12692  nn0enne  12694  nn0ehalf  12695  nn0o1gt2  12697  flodddiv4  12728  zeqzmulgcd  12772  gcdneg  12784  gcdaddm  12786  bezoutlemaz  12805  bezoutlembz  12806  dfgcd2  12816  gcddiv  12821  dvdssqim  12826  algcvgblem  12852  algcvga  12854  lcmneg  12877  coprmgcdb  12891  coprmdvds2  12896  qredeq  12899  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  prmind2  12923  dvdsnprmd  12928  prmgt1  12936  nprmdvds1  12944  divgcdodd  12947  euclemma  12950  prmdvdsexpr  12954  prmfac1  12956  prmndvdsfaclt  12960  crth  13031  eulerthlemh  13038  fermltl  13041  nnnn0modprm0  13063  coprimeprodsq2  13066  pythagtriplem2  13074  pcpremul  13101  pcdvdsb  13128  pc2dvds  13138  pc11  13139  dvdsprmpweqnn  13144  dvdsprmpweqle  13145  difsqpwdvds  13146  pcfac  13158  oddprmdvds  13162  prmpwdvds  13163  1arith  13175  4sqlem11  13209  4sqlem12  13210  prmlem0  13249  ballotfilemfrceq  13330  imasaddfnlemg  13694  erlecpbl  13712  xpsff1o  13729  imasmnd2  13818  grp1inv  13971  imasgrp2  13972  ghmpreima  14128  imasabl  14230  imasrng  14362  imasring  14478  dvdsrtr  14517  dvdsrmul1  14518  unitgrp  14532  znidomb  15102  tgtop  15294  tgidm  15300  neipsm  15380  restbasg  15394  tgrest  15395  tgcn  15434  tgcnp  15435  cnconst2  15459  cnconst  15460  cnptopresti  15464  txbasval  15493  txcnp  15497  txdis1cn  15504  bldisj  15627  xblm  15643  blssps  15653  blss  15654  blin2  15658  cnlimcim  15897  dveflem  15952  sincosq3sgn  16055  sincosq4sgn  16056  coseq0q4123  16061  sineq0re  16076  ioocosf1o  16082  logbgcd1irr  16203  birthdaylem1g  16225  pellexlem1  16229  pellexlem3  16231  mpodvdsmulf1o  16284  ppiublem1  16291  chtqub  16296  bclbnd  16307  bposlem1  16311  bposlem5  16315  zabsle1  16323  lgsdir2lem5  16356  lgsne0  16362  lgsdirnn0  16371  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem7  16392  gausslemma2d  16393  lgseisenlem2  16395  lgsquadlem1  16401  2lgslem1a1  16410  2lgslem1b  16413  2lgslem1c  16414  2lgs  16428  2lgsoddprmlem2  16430  upgrpredgv  16592  ausgrumgrien  16616  ausgrusgrien  16617  usgruspgrben  16632  uhgr2edg  16652  usgredg4  16661  ushgredgedg  16672  ushgredgedgloop  16674  edg0usgr  16693  uhgrspansubgrlem  16722  wlkl1loop  16804  wlk1walkdom  16805  wlklenvclwlk  16819  wlkres  16825  clwwlknonex2  16885  uzdcinzz  17031  subctctexmid  17235