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  4542  poltletr  5003  xp11m  5041  fvmptdf  5572  elfvmptrab1  5579  eusvobj2  5827  ovmpodf  5969  f1o2ndf1  6192  smoiso  6266  nnsseleq  6465  ecopovtrn  6594  ecopovtrng  6597  dom2lem  6734  fundmen  6768  fidifsnen  6832  findcard2  6851  findcard2s  6852  supisoex  6970  infglbti  6986  ordiso2  6996  updjud  7043  difinfsnlem  7060  enomnilem  7098  enmkvlem  7121  cc2lem  7203  addcanpig  7271  mulcanpig  7272  addnidpig  7273  ordpipqqs  7311  ltexnqq  7345  prarloclemlo  7431  genpcdl  7456  genpcuu  7457  mulnqprl  7505  mulnqpru  7506  distrlem1prl  7519  distrlem1pru  7520  distrlem4prl  7521  distrlem4pru  7522  distrlem5prl  7523  distrlem5pru  7524  ltsopr  7533  ltexprlemfl  7546  ltexprlemfu  7548  recexprlemss1l  7572  recexprlemss1u  7573  aptiprleml  7576  ltsrprg  7684  lttrsr  7699  mulextsr1lem  7717  axapti  7965  cnegexlem1  8069  le2add  8338  lt2add  8339  ltleadd  8340  lt2sub  8354  le2sub  8355  recexre  8472  reapti  8473  apreap  8481  reapcotr  8492  remulext1  8493  apreim  8497  apcotr  8501  mulext2  8507  recexap  8546  addltmul  9089  elnnz  9197  zleloe  9234  difgtsumgt  9256  nn0n0n1ge2b  9266  nn0lt2  9268  nn0le2is012  9269  zextlt  9279  uzind2  9299  supinfneg  9529  infsupneg  9530  eluzdc  9544  qreccl  9576  elpq  9582  xltnegi  9767  xnn0lenn0nn0  9797  iccid  9857  icoshft  9922  zltaddlt1le  9939  fzofzim  10119  qbtwnxr  10189  flqeqceilz  10249  modqmuladdnn0  10299  modfzo0difsn  10326  addmodlteq  10329  frec2uzrand  10336  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  facdiv  10647  facwordi  10649  faclbnd  10650  bcpasc  10675  seq3coll  10751  recvguniq  10933  abs00ap  11000  absext  11001  absnid  11011  cau3lem  11052  climuni  11230  2clim  11238  summodc  11320  fisumss  11329  fsumabs  11402  mertenslem2  11473  fprodssdc  11527  reeff1  11637  efieq1re  11708  dvdsmultr2  11769  dvdsleabs  11779  odd2np1lem  11805  odd2np1  11806  ltoddhalfle  11826  halfleoddlt  11827  m1expo  11833  nn0enne  11835  nn0ehalf  11836  nn0o1gt2  11838  flodddiv4  11867  zeqzmulgcd  11899  gcdneg  11911  gcdaddm  11913  bezoutlemaz  11932  bezoutlembz  11933  dfgcd2  11943  gcddiv  11948  dvdssqim  11953  algcvgblem  11977  algcvga  11979  lcmneg  12002  coprmgcdb  12016  coprmdvds2  12021  qredeq  12024  divgcdcoprm0  12029  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  prmind2  12048  dvdsnprmd  12053  prmgt1  12060  nprmdvds1  12068  divgcdodd  12071  euclemma  12074  prmdvdsexpr  12078  prmfac1  12080  prmndvdsfaclt  12084  crth  12152  eulerthlemh  12159  fermltl  12162  nnnn0modprm0  12183  coprimeprodsq2  12186  pythagtriplem2  12194  pcpremul  12221  pcdvdsb  12247  pc2dvds  12257  pc11  12258  dvdsprmpweqnn  12263  dvdsprmpweqle  12264  difsqpwdvds  12265  pcfac  12276  oddprmdvds  12280  prmpwdvds  12281  1arith  12293  tgtop  12668  tgidm  12674  neipsm  12754  restbasg  12768  tgrest  12769  tgcn  12808  tgcnp  12809  cnconst2  12833  cnconst  12834  cnptopresti  12838  txbasval  12867  txcnp  12871  txdis1cn  12878  bldisj  13001  xblm  13017  blssps  13027  blss  13028  blin2  13032  cnlimcim  13240  dveflem  13287  sincosq3sgn  13349  sincosq4sgn  13350  coseq0q4123  13355  ioocosf1o  13375  logbgcd1irr  13485  zabsle1  13500  lgsdir2lem5  13533  lgsne0  13539  lgsdirnn0  13548  uzdcinzz  13639  subctctexmid  13841