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  4550  poltletr  5011  xp11m  5049  fvmptdf  5583  elfvmptrab1  5590  eusvobj2  5839  ovmpodf  5984  f1o2ndf1  6207  smoiso  6281  nnsseleq  6480  ecopovtrn  6610  ecopovtrng  6613  dom2lem  6750  fundmen  6784  fidifsnen  6848  findcard2  6867  findcard2s  6868  supisoex  6986  infglbti  7002  ordiso2  7012  updjud  7059  difinfsnlem  7076  enomnilem  7114  enmkvlem  7137  cc2lem  7228  addcanpig  7296  mulcanpig  7297  addnidpig  7298  ordpipqqs  7336  ltexnqq  7370  prarloclemlo  7456  genpcdl  7481  genpcuu  7482  mulnqprl  7530  mulnqpru  7531  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  distrlem5prl  7548  distrlem5pru  7549  ltsopr  7558  ltexprlemfl  7571  ltexprlemfu  7573  recexprlemss1l  7597  recexprlemss1u  7598  aptiprleml  7601  ltsrprg  7709  lttrsr  7724  mulextsr1lem  7742  axapti  7990  cnegexlem1  8094  le2add  8363  lt2add  8364  ltleadd  8365  lt2sub  8379  le2sub  8380  recexre  8497  reapti  8498  apreap  8506  reapcotr  8517  remulext1  8518  apreim  8522  apcotr  8526  mulext2  8532  recexap  8571  addltmul  9114  elnnz  9222  zleloe  9259  difgtsumgt  9281  nn0n0n1ge2b  9291  nn0lt2  9293  nn0le2is012  9294  zextlt  9304  uzind2  9324  supinfneg  9554  infsupneg  9555  eluzdc  9569  qreccl  9601  elpq  9607  xltnegi  9792  xnn0lenn0nn0  9822  iccid  9882  icoshft  9947  zltaddlt1le  9964  fzofzim  10144  qbtwnxr  10214  flqeqceilz  10274  modqmuladdnn0  10324  modfzo0difsn  10351  addmodlteq  10354  frec2uzrand  10361  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  facdiv  10672  facwordi  10674  faclbnd  10675  bcpasc  10700  seq3coll  10777  recvguniq  10959  abs00ap  11026  absext  11027  absnid  11037  cau3lem  11078  climuni  11256  2clim  11264  summodc  11346  fisumss  11355  fsumabs  11428  mertenslem2  11499  fprodssdc  11553  reeff1  11663  efieq1re  11734  dvdsmultr2  11795  dvdsleabs  11805  odd2np1lem  11831  odd2np1  11832  ltoddhalfle  11852  halfleoddlt  11853  m1expo  11859  nn0enne  11861  nn0ehalf  11862  nn0o1gt2  11864  flodddiv4  11893  zeqzmulgcd  11925  gcdneg  11937  gcdaddm  11939  bezoutlemaz  11958  bezoutlembz  11959  dfgcd2  11969  gcddiv  11974  dvdssqim  11979  algcvgblem  12003  algcvga  12005  lcmneg  12028  coprmgcdb  12042  coprmdvds2  12047  qredeq  12050  divgcdcoprm0  12055  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  prmind2  12074  dvdsnprmd  12079  prmgt1  12086  nprmdvds1  12094  divgcdodd  12097  euclemma  12100  prmdvdsexpr  12104  prmfac1  12106  prmndvdsfaclt  12110  crth  12178  eulerthlemh  12185  fermltl  12188  nnnn0modprm0  12209  coprimeprodsq2  12212  pythagtriplem2  12220  pcpremul  12247  pcdvdsb  12273  pc2dvds  12283  pc11  12284  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  difsqpwdvds  12291  pcfac  12302  oddprmdvds  12306  prmpwdvds  12307  1arith  12319  tgtop  12862  tgidm  12868  neipsm  12948  restbasg  12962  tgrest  12963  tgcn  13002  tgcnp  13003  cnconst2  13027  cnconst  13028  cnptopresti  13032  txbasval  13061  txcnp  13065  txdis1cn  13072  bldisj  13195  xblm  13211  blssps  13221  blss  13222  blin2  13226  cnlimcim  13434  dveflem  13481  sincosq3sgn  13543  sincosq4sgn  13544  coseq0q4123  13549  ioocosf1o  13569  logbgcd1irr  13679  zabsle1  13694  lgsdir2lem5  13727  lgsne0  13733  lgsdirnn0  13742  uzdcinzz  13833  subctctexmid  14034