Theorem sylbid 149

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 143	. 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 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  nlimsucg  4489  poltletr  4947  xp11m  4985  fvmptdf  5516  elfvmptrab1  5523  eusvobj2  5768  ovmpodf  5910  f1o2ndf1  6133  smoiso  6207  nnsseleq  6405  ecopovtrn  6534  ecopovtrng  6537  dom2lem  6674  fundmen  6708  fidifsnen  6772  findcard2  6791  findcard2s  6792  supisoex  6904  infglbti  6920  ordiso2  6928  updjud  6975  difinfsnlem  6992  enomnilem  7018  enmkvlem  7043  cc2lem  7098  addcanpig  7166  mulcanpig  7167  addnidpig  7168  ordpipqqs  7206  ltexnqq  7240  prarloclemlo  7326  genpcdl  7351  genpcuu  7352  mulnqprl  7400  mulnqpru  7401  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  distrlem5prl  7418  distrlem5pru  7419  ltsopr  7428  ltexprlemfl  7441  ltexprlemfu  7443  recexprlemss1l  7467  recexprlemss1u  7468  aptiprleml  7471  ltsrprg  7579  lttrsr  7594  mulextsr1lem  7612  axapti  7859  cnegexlem1  7961  le2add  8230  lt2add  8231  ltleadd  8232  lt2sub  8246  le2sub  8247  recexre  8364  reapti  8365  apreap  8373  reapcotr  8384  remulext1  8385  apreim  8389  apcotr  8393  mulext2  8399  recexap  8438  addltmul  8980  elnnz  9088  zleloe  9125  nn0n0n1ge2b  9154  nn0lt2  9156  nn0le2is012  9157  zextlt  9167  uzind2  9187  supinfneg  9417  infsupneg  9418  eluzdc  9431  qreccl  9461  elpq  9467  xltnegi  9648  xnn0lenn0nn0  9678  iccid  9738  icoshft  9803  zltaddlt1le  9820  fzofzim  9996  qbtwnxr  10066  flqeqceilz  10122  modqmuladdnn0  10172  modfzo0difsn  10199  addmodlteq  10202  frec2uzrand  10209  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  facdiv  10516  facwordi  10518  faclbnd  10519  bcpasc  10544  seq3coll  10617  recvguniq  10799  abs00ap  10866  absext  10867  absnid  10877  cau3lem  10918  climuni  11094  2clim  11102  summodc  11184  fisumss  11193  fsumabs  11266  mertenslem2  11337  reeff1  11443  efieq1re  11514  dvdsmultr2  11569  dvdsleabs  11579  odd2np1lem  11605  odd2np1  11606  ltoddhalfle  11626  halfleoddlt  11627  m1expo  11633  nn0enne  11635  nn0ehalf  11636  nn0o1gt2  11638  flodddiv4  11667  zeqzmulgcd  11695  gcdneg  11706  gcdaddm  11708  bezoutlemaz  11727  bezoutlembz  11728  dfgcd2  11738  gcddiv  11743  dvdssqim  11748  algcvgblem  11766  algcvga  11768  lcmneg  11791  coprmgcdb  11805  coprmdvds2  11810  qredeq  11813  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  prmind2  11837  dvdsnprmd  11842  prmgt1  11848  nprmdvds1  11856  divgcdodd  11857  euclemma  11860  prmdvdsexpr  11864  prmfac1  11866  prmndvdsfaclt  11870  crth  11936  tgtop  12276  tgidm  12282  neipsm  12362  restbasg  12376  tgrest  12377  tgcn  12416  tgcnp  12417  cnconst2  12441  cnconst  12442  cnptopresti  12446  txbasval  12475  txcnp  12479  txdis1cn  12486  bldisj  12609  xblm  12625  blssps  12635  blss  12636  blin2  12640  cnlimcim  12848  dveflem  12895  sincosq3sgn  12957  sincosq4sgn  12958  coseq0q4123  12963  ioocosf1o  12983  logbgcd1irr  13092  uzdcinzz  13176  subctctexmid  13369