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  4713  ssrelrn  4972  poltletr  5188  xp11m  5226  fvmptdf  5793  elfvmptrab1  5801  eusvobj2  6071  ovmpodf  6220  elovmporab  6289  elovmporab1w  6290  f1o2ndf1  6464  suppssdc  6500  suppssrst  6501  suppssrgst  6502  smoiso  6573  nnsseleq  6774  ecopovtrn  6906  ecopovtrng  6909  dom2lem  7058  fundmen  7094  dom1o  7116  fidifsnen  7172  findcard2  7193  findcard2s  7194  supisoex  7349  infglbti  7365  ordiso2  7375  updjud  7422  difinfsnlem  7439  enomnilem  7478  enmkvlem  7501  netap  7620  2omotaplemap  7623  cc2lem  7632  addcanpig  7701  mulcanpig  7702  addnidpig  7703  ordpipqqs  7741  ltexnqq  7775  prarloclemlo  7861  genpcdl  7886  genpcuu  7887  mulnqprl  7935  mulnqpru  7936  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  distrlem5prl  7953  distrlem5pru  7954  ltsopr  7963  ltexprlemfl  7976  ltexprlemfu  7978  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  ltsrprg  8114  lttrsr  8129  mulextsr1lem  8147  axapti  8396  cnegexlem1  8502  le2add  8773  lt2add  8774  ltleadd  8775  lt2sub  8789  le2sub  8790  recexre  8908  reapti  8909  apreap  8917  reapcotr  8928  remulext1  8929  apreim  8933  apcotr  8937  mulext2  8943  recexap  8983  addltmul  9546  elnnz  9658  zleloe  9695  difgtsumgt  9718  nn0n0n1ge2b  9729  nn0lt2  9731  nn0le2is012  9732  zextlt  9742  uzind2  9762  supinfneg  10004  infsupneg  10005  eluzdc  10019  qreccl  10051  elpq  10059  xltnegi  10247  xnn0lenn0nn0  10277  iccid  10337  icoshft  10402  zltaddlt1le  10420  fzofzim  10610  qbtwnxr  10702  flqeqceilz  10768  modqmuladdnn0  10818  modfzo0difsn  10845  addmodlteq  10848  frec2uzrand  10855  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  seqf1oglem1  10969  facdiv  11190  facwordi  11192  faclbnd  11193  bcpasc  11218  seq3coll  11308  fundm2domnop0  11314  fstwrdne  11357  elovmpowrd  11360  lswlgt0cl  11371  ccatrn  11391  ccatalpha  11395  swrdnd  11445  swrdswrd  11491  wrd2ind  11509  swrdccatin1  11511  pfxccatin12lem2a  11513  pfxccat3  11520  swrdccat  11521  swrdccat3blem  11525  reuccatpfxs1lem  11532  recvguniq  11775  abs00ap  11842  absext  11843  absnid  11853  cau3lem  11895  climuni  12075  2clim  12083  summodc  12166  fisumss  12175  fsumabs  12248  mertenslem2  12319  fprodssdc  12373  reeff1  12483  efieq1re  12555  dvdsmultr2  12616  dvdsleabs  12628  odd2np1lem  12655  odd2np1  12656  ltoddhalfle  12676  halfleoddlt  12677  m1expo  12683  nn0enne  12685  nn0ehalf  12686  nn0o1gt2  12688  flodddiv4  12719  zeqzmulgcd  12763  gcdneg  12775  gcdaddm  12777  bezoutlemaz  12796  bezoutlembz  12797  dfgcd2  12807  gcddiv  12812  dvdssqim  12817  algcvgblem  12843  algcvga  12845  lcmneg  12868  coprmgcdb  12882  coprmdvds2  12887  qredeq  12890  divgcdcoprm0  12895  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  prmind2  12914  dvdsnprmd  12919  prmgt1  12927  nprmdvds1  12935  divgcdodd  12938  euclemma  12941  prmdvdsexpr  12945  prmfac1  12947  prmndvdsfaclt  12951  crth  13022  eulerthlemh  13029  fermltl  13032  nnnn0modprm0  13054  coprimeprodsq2  13057  pythagtriplem2  13065  pcpremul  13092  pcdvdsb  13119  pc2dvds  13129  pc11  13130  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  difsqpwdvds  13137  pcfac  13149  oddprmdvds  13153  prmpwdvds  13154  1arith  13166  4sqlem11  13200  4sqlem12  13201  prmlem0  13240  ballotfilemfrceq  13321  imasaddfnlemg  13684  erlecpbl  13702  xpsff1o  13719  imasmnd2  13808  grp1inv  13961  imasgrp2  13962  ghmpreima  14118  imasabl  14189  imasrng  14304  imasring  14418  dvdsrtr  14457  dvdsrmul1  14458  unitgrp  14472  znidomb  15042  tgtop  15218  tgidm  15224  neipsm  15304  restbasg  15318  tgrest  15319  tgcn  15358  tgcnp  15359  cnconst2  15383  cnconst  15384  cnptopresti  15388  txbasval  15417  txcnp  15421  txdis1cn  15428  bldisj  15551  xblm  15567  blssps  15577  blss  15578  blin2  15582  cnlimcim  15821  dveflem  15876  sincosq3sgn  15979  sincosq4sgn  15980  coseq0q4123  15985  ioocosf1o  16005  logbgcd1irr  16122  birthdaylem1g  16144  pellexlem1  16148  pellexlem3  16150  mpodvdsmulf1o  16185  ppiublem1  16192  bclbnd  16205  bposlem1  16209  bposlem5  16213  zabsle1  16216  lgsdir2lem5  16249  lgsne0  16255  lgsdirnn0  16264  gausslemma2dlem0i  16274  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem7  16285  gausslemma2d  16286  lgseisenlem2  16288  lgsquadlem1  16294  2lgslem1a1  16303  2lgslem1b  16306  2lgslem1c  16307  2lgs  16321  2lgsoddprmlem2  16323  upgrpredgv  16485  ausgrumgrien  16509  ausgrusgrien  16510  usgruspgrben  16525  uhgr2edg  16545  usgredg4  16554  ushgredgedg  16565  ushgredgedgloop  16567  edg0usgr  16586  uhgrspansubgrlem  16615  wlkl1loop  16697  wlk1walkdom  16698  wlklenvclwlk  16712  wlkres  16718  clwwlknonex2  16778  uzdcinzz  16924  subctctexmid  17128