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 ) )

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  3655  ssprsseq  3840  nlimsucg  4670  ssrelrn  4928  poltletr  5144  xp11m  5182  fvmptdf  5743  elfvmptrab1  5750  eusvobj2  6014  ovmpodf  6163  elovmporab  6232  elovmporab1w  6233  f1o2ndf1  6402  suppssdc  6438  suppssrst  6439  suppssrgst  6440  smoiso  6511  nnsseleq  6712  ecopovtrn  6844  ecopovtrng  6847  dom2lem  6988  fundmen  7024  dom1o  7045  fidifsnen  7100  findcard2  7121  findcard2s  7122  supisoex  7268  infglbti  7284  ordiso2  7294  updjud  7341  difinfsnlem  7358  enomnilem  7397  enmkvlem  7420  netap  7533  2omotaplemap  7536  cc2lem  7545  addcanpig  7614  mulcanpig  7615  addnidpig  7616  ordpipqqs  7654  ltexnqq  7688  prarloclemlo  7774  genpcdl  7799  genpcuu  7800  mulnqprl  7848  mulnqpru  7849  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  distrlem5prl  7866  distrlem5pru  7867  ltsopr  7876  ltexprlemfl  7889  ltexprlemfu  7891  recexprlemss1l  7915  recexprlemss1u  7916  aptiprleml  7919  ltsrprg  8027  lttrsr  8042  mulextsr1lem  8060  axapti  8309  cnegexlem1  8413  le2add  8683  lt2add  8684  ltleadd  8685  lt2sub  8699  le2sub  8700  recexre  8817  reapti  8818  apreap  8826  reapcotr  8837  remulext1  8838  apreim  8842  apcotr  8846  mulext2  8852  recexap  8892  addltmul  9440  elnnz  9550  zleloe  9587  difgtsumgt  9610  nn0n0n1ge2b  9620  nn0lt2  9622  nn0le2is012  9623  zextlt  9633  uzind2  9653  supinfneg  9890  infsupneg  9891  eluzdc  9905  qreccl  9937  elpq  9944  xltnegi  10131  xnn0lenn0nn0  10161  iccid  10221  icoshft  10286  zltaddlt1le  10304  fzofzim  10490  qbtwnxr  10580  flqeqceilz  10643  modqmuladdnn0  10693  modfzo0difsn  10720  addmodlteq  10723  frec2uzrand  10730  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  seqf1oglem1  10844  facdiv  11063  facwordi  11065  faclbnd  11066  bcpasc  11091  seq3coll  11169  fundm2domnop0  11175  fstwrdne  11218  elovmpowrd  11221  lswlgt0cl  11232  ccatrn  11252  ccatalpha  11256  swrdnd  11306  swrdswrd  11352  wrd2ind  11370  swrdccatin1  11372  pfxccatin12lem2a  11374  pfxccat3  11381  swrdccat  11382  swrdccat3blem  11386  reuccatpfxs1lem  11393  recvguniq  11635  abs00ap  11702  absext  11703  absnid  11713  cau3lem  11754  climuni  11933  2clim  11941  summodc  12024  fisumss  12033  fsumabs  12106  mertenslem2  12177  fprodssdc  12231  reeff1  12341  efieq1re  12413  dvdsmultr2  12474  dvdsleabs  12486  odd2np1lem  12513  odd2np1  12514  ltoddhalfle  12534  halfleoddlt  12535  m1expo  12541  nn0enne  12543  nn0ehalf  12544  nn0o1gt2  12546  flodddiv4  12577  zeqzmulgcd  12621  gcdneg  12633  gcdaddm  12635  bezoutlemaz  12654  bezoutlembz  12655  dfgcd2  12665  gcddiv  12670  dvdssqim  12675  algcvgblem  12701  algcvga  12703  lcmneg  12726  coprmgcdb  12740  coprmdvds2  12745  qredeq  12748  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  prmind2  12772  dvdsnprmd  12777  prmgt1  12784  nprmdvds1  12792  divgcdodd  12795  euclemma  12798  prmdvdsexpr  12802  prmfac1  12804  prmndvdsfaclt  12808  crth  12876  eulerthlemh  12883  fermltl  12886  nnnn0modprm0  12908  coprimeprodsq2  12911  pythagtriplem2  12919  pcpremul  12946  pcdvdsb  12973  pc2dvds  12983  pc11  12984  dvdsprmpweqnn  12989  dvdsprmpweqle  12990  difsqpwdvds  12991  pcfac  13003  oddprmdvds  13007  prmpwdvds  13008  1arith  13020  4sqlem11  13054  4sqlem12  13055  imasaddfnlemg  13477  erlecpbl  13495  xpsff1o  13512  imasmnd2  13615  grp1inv  13770  imasgrp2  13777  ghmpreima  13933  imasabl  14003  imasrng  14050  imasring  14158  dvdsrtr  14196  dvdsrmul1  14197  unitgrp  14211  znidomb  14754  tgtop  14879  tgidm  14885  neipsm  14965  restbasg  14979  tgrest  14980  tgcn  15019  tgcnp  15020  cnconst2  15044  cnconst  15045  cnptopresti  15049  txbasval  15078  txcnp  15082  txdis1cn  15089  bldisj  15212  xblm  15228  blssps  15238  blss  15239  blin2  15243  cnlimcim  15482  dveflem  15537  sincosq3sgn  15639  sincosq4sgn  15640  coseq0q4123  15645  ioocosf1o  15665  logbgcd1irr  15778  pellexlem1  15791  pellexlem3  15793  mpodvdsmulf1o  15804  zabsle1  15818  lgsdir2lem5  15851  lgsne0  15857  lgsdirnn0  15866  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  gausslemma2dlem2  15881  gausslemma2dlem7  15887  gausslemma2d  15888  lgseisenlem2  15890  lgsquadlem1  15896  2lgslem1a1  15905  2lgslem1b  15908  2lgslem1c  15909  2lgs  15923  2lgsoddprmlem2  15925  upgrpredgv  16087  ausgrumgrien  16111  ausgrusgrien  16112  usgruspgrben  16127  uhgr2edg  16147  usgredg4  16156  ushgredgedg  16167  ushgredgedgloop  16169  edg0usgr  16188  uhgrspansubgrlem  16217  wlkl1loop  16299  wlk1walkdom  16300  wlklenvclwlk  16314  wlkres  16320  clwwlknonex2  16380  uzdcinzz  16516  subctctexmid  16722