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  3625  ssprsseq  3806  nlimsucg  4632  ssrelrn  4888  poltletr  5102  xp11m  5140  fvmptdf  5690  elfvmptrab1  5697  eusvobj2  5953  ovmpodf  6100  elovmporab  6169  elovmporab1w  6170  f1o2ndf1  6337  smoiso  6411  nnsseleq  6610  ecopovtrn  6742  ecopovtrng  6745  dom2lem  6886  fundmen  6922  fidifsnen  6993  findcard2  7012  findcard2s  7013  supisoex  7137  infglbti  7153  ordiso2  7163  updjud  7210  difinfsnlem  7227  enomnilem  7266  enmkvlem  7289  netap  7401  2omotaplemap  7404  cc2lem  7413  addcanpig  7482  mulcanpig  7483  addnidpig  7484  ordpipqqs  7522  ltexnqq  7556  prarloclemlo  7642  genpcdl  7667  genpcuu  7668  mulnqprl  7716  mulnqpru  7717  distrlem1prl  7730  distrlem1pru  7731  distrlem4prl  7732  distrlem4pru  7733  distrlem5prl  7734  distrlem5pru  7735  ltsopr  7744  ltexprlemfl  7757  ltexprlemfu  7759  recexprlemss1l  7783  recexprlemss1u  7784  aptiprleml  7787  ltsrprg  7895  lttrsr  7910  mulextsr1lem  7928  axapti  8178  cnegexlem1  8282  le2add  8552  lt2add  8553  ltleadd  8554  lt2sub  8568  le2sub  8569  recexre  8686  reapti  8687  apreap  8695  reapcotr  8706  remulext1  8707  apreim  8711  apcotr  8715  mulext2  8721  recexap  8761  addltmul  9309  elnnz  9417  zleloe  9454  difgtsumgt  9477  nn0n0n1ge2b  9487  nn0lt2  9489  nn0le2is012  9490  zextlt  9500  uzind2  9520  supinfneg  9751  infsupneg  9752  eluzdc  9766  qreccl  9798  elpq  9805  xltnegi  9992  xnn0lenn0nn0  10022  iccid  10082  icoshft  10147  zltaddlt1le  10164  fzofzim  10349  qbtwnxr  10437  flqeqceilz  10500  modqmuladdnn0  10550  modfzo0difsn  10577  addmodlteq  10580  frec2uzrand  10587  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  seqf1oglem1  10701  facdiv  10920  facwordi  10922  faclbnd  10923  bcpasc  10948  seq3coll  11024  fundm2domnop0  11027  fstwrdne  11069  elovmpowrd  11072  lswlgt0cl  11083  ccatrn  11103  swrdnd  11150  swrdswrd  11196  wrd2ind  11214  swrdccatin1  11216  pfxccatin12lem2a  11218  pfxccat3  11225  swrdccat  11226  swrdccat3blem  11230  reuccatpfxs1lem  11237  recvguniq  11421  abs00ap  11488  absext  11489  absnid  11499  cau3lem  11540  climuni  11719  2clim  11727  summodc  11809  fisumss  11818  fsumabs  11891  mertenslem2  11962  fprodssdc  12016  reeff1  12126  efieq1re  12198  dvdsmultr2  12259  dvdsleabs  12271  odd2np1lem  12298  odd2np1  12299  ltoddhalfle  12319  halfleoddlt  12320  m1expo  12326  nn0enne  12328  nn0ehalf  12329  nn0o1gt2  12331  flodddiv4  12362  zeqzmulgcd  12406  gcdneg  12418  gcdaddm  12420  bezoutlemaz  12439  bezoutlembz  12440  dfgcd2  12450  gcddiv  12455  dvdssqim  12460  algcvgblem  12486  algcvga  12488  lcmneg  12511  coprmgcdb  12525  coprmdvds2  12530  qredeq  12533  divgcdcoprm0  12538  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  prmind2  12557  dvdsnprmd  12562  prmgt1  12569  nprmdvds1  12577  divgcdodd  12580  euclemma  12583  prmdvdsexpr  12587  prmfac1  12589  prmndvdsfaclt  12593  crth  12661  eulerthlemh  12668  fermltl  12671  nnnn0modprm0  12693  coprimeprodsq2  12696  pythagtriplem2  12704  pcpremul  12731  pcdvdsb  12758  pc2dvds  12768  pc11  12769  dvdsprmpweqnn  12774  dvdsprmpweqle  12775  difsqpwdvds  12776  pcfac  12788  oddprmdvds  12792  prmpwdvds  12793  1arith  12805  4sqlem11  12839  4sqlem12  12840  imasaddfnlemg  13261  erlecpbl  13279  xpsff1o  13296  imasmnd2  13399  grp1inv  13554  imasgrp2  13561  ghmpreima  13717  imasabl  13787  imasrng  13833  imasring  13941  dvdsrtr  13978  dvdsrmul1  13979  unitgrp  13993  znidomb  14535  tgtop  14655  tgidm  14661  neipsm  14741  restbasg  14755  tgrest  14756  tgcn  14795  tgcnp  14796  cnconst2  14820  cnconst  14821  cnptopresti  14825  txbasval  14854  txcnp  14858  txdis1cn  14865  bldisj  14988  xblm  15004  blssps  15014  blss  15015  blin2  15019  cnlimcim  15258  dveflem  15313  sincosq3sgn  15415  sincosq4sgn  15416  coseq0q4123  15421  ioocosf1o  15441  logbgcd1irr  15554  mpodvdsmulf1o  15577  zabsle1  15591  lgsdir2lem5  15624  lgsne0  15630  lgsdirnn0  15639  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  gausslemma2dlem2  15654  gausslemma2dlem7  15660  gausslemma2d  15661  lgseisenlem2  15663  lgsquadlem1  15669  2lgslem1a1  15678  2lgslem1b  15681  2lgslem1c  15682  2lgs  15696  2lgsoddprmlem2  15698  upgrpredgv  15850  uzdcinzz  15934  dom1o  16128  subctctexmid  16139