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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3imtr4d  202  nlimsucg  4397  poltletr  4847  xp11m  4884  fvmptdf  5405  eusvobj2  5654  ovmpt2df  5792  f1o2ndf1  6009  smoiso  6083  nnsseleq  6278  ecopovtrn  6405  ecopovtrng  6408  dom2lem  6545  fundmen  6579  fidifsnen  6642  findcard2  6661  findcard2s  6662  supisoex  6760  infglbti  6776  ordiso2  6784  updjud  6829  enomnilem  6857  addcanpig  6956  mulcanpig  6957  addnidpig  6958  ordpipqqs  6996  ltexnqq  7030  prarloclemlo  7116  genpcdl  7141  genpcuu  7142  mulnqprl  7190  mulnqpru  7191  distrlem1prl  7204  distrlem1pru  7205  distrlem4prl  7206  distrlem4pru  7207  distrlem5prl  7208  distrlem5pru  7209  ltsopr  7218  ltexprlemfl  7231  ltexprlemfu  7233  recexprlemss1l  7257  recexprlemss1u  7258  aptiprleml  7261  ltsrprg  7356  lttrsr  7371  mulextsr1lem  7388  axapti  7620  cnegexlem1  7720  le2add  7985  lt2add  7986  ltleadd  7987  lt2sub  8001  le2sub  8002  recexre  8118  reapti  8119  apreap  8127  reapcotr  8138  remulext1  8139  apreim  8143  apcotr  8147  mulext2  8153  recexap  8185  addltmul  8715  elnnz  8823  zleloe  8860  nn0n0n1ge2b  8889  nn0lt2  8891  zextlt  8901  uzind2  8921  supinfneg  9146  infsupneg  9147  eluzdc  9160  qreccl  9190  xltnegi  9360  iccid  9406  icoshft  9470  zltaddlt1le  9486  fzofzim  9662  qbtwnxr  9732  flqeqceilz  9788  modqmuladdnn0  9838  modfzo0difsn  9865  addmodlteq  9868  frec2uzrand  9875  frecuzrdgtcl  9882  frecuzrdgfunlem  9889  facdiv  10209  facwordi  10211  faclbnd  10212  bcpasc  10237  iseqcoll  10310  recvguniq  10491  abs00ap  10558  absext  10559  absnid  10569  cau3lem  10610  climuni  10744  2clim  10752  isummo  10836  fisumss  10847  fsumabs  10922  mertenslem2  10993  reeff1  11054  efieq1re  11124  dvdsmultr2  11177  dvdsleabs  11187  odd2np1lem  11213  odd2np1  11214  ltoddhalfle  11234  halfleoddlt  11235  m1expo  11241  nn0enne  11243  nn0ehalf  11244  nn0o1gt2  11246  flodddiv4  11275  zeqzmulgcd  11303  gcdneg  11314  gcdaddm  11316  bezoutlemaz  11333  bezoutlembz  11334  dfgcd2  11344  gcddiv  11349  dvdssqim  11354  algcvgblem  11372  algcvga  11374  lcmneg  11397  coprmgcdb  11411  coprmdvds2  11416  qredeq  11419  divgcdcoprm0  11424  divgcdcoprmex  11425  cncongr1  11426  cncongr2  11427  prmind2  11443  dvdsnprmd  11448  prmgt1  11454  nprmdvds1  11462  divgcdodd  11463  euclemma  11466  prmdvdsexpr  11470  prmfac1  11472  prmndvdsfaclt  11476  crth  11541  tgtop  11831  tgidm  11837  neipsm  11917  uzdcinzz  12002