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  3604  nlimsucg  4602  poltletr  5070  xp11m  5108  fvmptdf  5649  elfvmptrab1  5656  eusvobj2  5908  ovmpodf  6054  elovmporab  6123  elovmporab1w  6124  f1o2ndf1  6286  smoiso  6360  nnsseleq  6559  ecopovtrn  6691  ecopovtrng  6694  dom2lem  6831  fundmen  6865  fidifsnen  6931  findcard2  6950  findcard2s  6951  supisoex  7075  infglbti  7091  ordiso2  7101  updjud  7148  difinfsnlem  7165  enomnilem  7204  enmkvlem  7227  netap  7321  2omotaplemap  7324  cc2lem  7333  addcanpig  7401  mulcanpig  7402  addnidpig  7403  ordpipqqs  7441  ltexnqq  7475  prarloclemlo  7561  genpcdl  7586  genpcuu  7587  mulnqprl  7635  mulnqpru  7636  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  distrlem5prl  7653  distrlem5pru  7654  ltsopr  7663  ltexprlemfl  7676  ltexprlemfu  7678  recexprlemss1l  7702  recexprlemss1u  7703  aptiprleml  7706  ltsrprg  7814  lttrsr  7829  mulextsr1lem  7847  axapti  8097  cnegexlem1  8201  le2add  8471  lt2add  8472  ltleadd  8473  lt2sub  8487  le2sub  8488  recexre  8605  reapti  8606  apreap  8614  reapcotr  8625  remulext1  8626  apreim  8630  apcotr  8634  mulext2  8640  recexap  8680  addltmul  9228  elnnz  9336  zleloe  9373  difgtsumgt  9395  nn0n0n1ge2b  9405  nn0lt2  9407  nn0le2is012  9408  zextlt  9418  uzind2  9438  supinfneg  9669  infsupneg  9670  eluzdc  9684  qreccl  9716  elpq  9723  xltnegi  9910  xnn0lenn0nn0  9940  iccid  10000  icoshft  10065  zltaddlt1le  10082  fzofzim  10264  qbtwnxr  10347  flqeqceilz  10410  modqmuladdnn0  10460  modfzo0difsn  10487  addmodlteq  10490  frec2uzrand  10497  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  seqf1oglem1  10611  facdiv  10830  facwordi  10832  faclbnd  10833  bcpasc  10858  seq3coll  10934  fstwrdne  10973  elovmpowrd  10976  recvguniq  11160  abs00ap  11227  absext  11228  absnid  11238  cau3lem  11279  climuni  11458  2clim  11466  summodc  11548  fisumss  11557  fsumabs  11630  mertenslem2  11701  fprodssdc  11755  reeff1  11865  efieq1re  11937  dvdsmultr2  11998  dvdsleabs  12010  odd2np1lem  12037  odd2np1  12038  ltoddhalfle  12058  halfleoddlt  12059  m1expo  12065  nn0enne  12067  nn0ehalf  12068  nn0o1gt2  12070  flodddiv4  12101  zeqzmulgcd  12137  gcdneg  12149  gcdaddm  12151  bezoutlemaz  12170  bezoutlembz  12171  dfgcd2  12181  gcddiv  12186  dvdssqim  12191  algcvgblem  12217  algcvga  12219  lcmneg  12242  coprmgcdb  12256  coprmdvds2  12261  qredeq  12264  divgcdcoprm0  12269  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  prmind2  12288  dvdsnprmd  12293  prmgt1  12300  nprmdvds1  12308  divgcdodd  12311  euclemma  12314  prmdvdsexpr  12318  prmfac1  12320  prmndvdsfaclt  12324  crth  12392  eulerthlemh  12399  fermltl  12402  nnnn0modprm0  12424  coprimeprodsq2  12427  pythagtriplem2  12435  pcpremul  12462  pcdvdsb  12489  pc2dvds  12499  pc11  12500  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  difsqpwdvds  12507  pcfac  12519  oddprmdvds  12523  prmpwdvds  12524  1arith  12536  4sqlem11  12570  4sqlem12  12571  imasaddfnlemg  12957  erlecpbl  12975  xpsff1o  12992  grp1inv  13239  imasgrp2  13240  ghmpreima  13396  imasabl  13466  imasrng  13512  imasring  13620  dvdsrtr  13657  dvdsrmul1  13658  unitgrp  13672  znidomb  14214  tgtop  14304  tgidm  14310  neipsm  14390  restbasg  14404  tgrest  14405  tgcn  14444  tgcnp  14445  cnconst2  14469  cnconst  14470  cnptopresti  14474  txbasval  14503  txcnp  14507  txdis1cn  14514  bldisj  14637  xblm  14653  blssps  14663  blss  14664  blin2  14668  cnlimcim  14907  dveflem  14962  sincosq3sgn  15064  sincosq4sgn  15065  coseq0q4123  15070  ioocosf1o  15090  logbgcd1irr  15203  mpodvdsmulf1o  15226  zabsle1  15240  lgsdir2lem5  15273  lgsne0  15279  lgsdirnn0  15288  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem2  15312  lgsquadlem1  15318  2lgslem1a1  15327  2lgslem1b  15330  2lgslem1c  15331  2lgs  15345  2lgsoddprmlem2  15347  uzdcinzz  15444  subctctexmid  15645