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  3615  nlimsucg  4615  poltletr  5084  xp11m  5122  fvmptdf  5669  elfvmptrab1  5676  eusvobj2  5932  ovmpodf  6079  elovmporab  6148  elovmporab1w  6149  f1o2ndf1  6316  smoiso  6390  nnsseleq  6589  ecopovtrn  6721  ecopovtrng  6724  dom2lem  6865  fundmen  6900  fidifsnen  6969  findcard2  6988  findcard2s  6989  supisoex  7113  infglbti  7129  ordiso2  7139  updjud  7186  difinfsnlem  7203  enomnilem  7242  enmkvlem  7265  netap  7368  2omotaplemap  7371  cc2lem  7380  addcanpig  7449  mulcanpig  7450  addnidpig  7451  ordpipqqs  7489  ltexnqq  7523  prarloclemlo  7609  genpcdl  7634  genpcuu  7635  mulnqprl  7683  mulnqpru  7684  distrlem1prl  7697  distrlem1pru  7698  distrlem4prl  7699  distrlem4pru  7700  distrlem5prl  7701  distrlem5pru  7702  ltsopr  7711  ltexprlemfl  7724  ltexprlemfu  7726  recexprlemss1l  7750  recexprlemss1u  7751  aptiprleml  7754  ltsrprg  7862  lttrsr  7877  mulextsr1lem  7895  axapti  8145  cnegexlem1  8249  le2add  8519  lt2add  8520  ltleadd  8521  lt2sub  8535  le2sub  8536  recexre  8653  reapti  8654  apreap  8662  reapcotr  8673  remulext1  8674  apreim  8678  apcotr  8682  mulext2  8688  recexap  8728  addltmul  9276  elnnz  9384  zleloe  9421  difgtsumgt  9444  nn0n0n1ge2b  9454  nn0lt2  9456  nn0le2is012  9457  zextlt  9467  uzind2  9487  supinfneg  9718  infsupneg  9719  eluzdc  9733  qreccl  9765  elpq  9772  xltnegi  9959  xnn0lenn0nn0  9989  iccid  10049  icoshft  10114  zltaddlt1le  10131  fzofzim  10314  qbtwnxr  10402  flqeqceilz  10465  modqmuladdnn0  10515  modfzo0difsn  10542  addmodlteq  10545  frec2uzrand  10552  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  seqf1oglem1  10666  facdiv  10885  facwordi  10887  faclbnd  10888  bcpasc  10913  seq3coll  10989  fundm2domnop0  10992  fstwrdne  11034  elovmpowrd  11037  lswlgt0cl  11048  ccatrn  11068  swrdnd  11115  recvguniq  11339  abs00ap  11406  absext  11407  absnid  11417  cau3lem  11458  climuni  11637  2clim  11645  summodc  11727  fisumss  11736  fsumabs  11809  mertenslem2  11880  fprodssdc  11934  reeff1  12044  efieq1re  12116  dvdsmultr2  12177  dvdsleabs  12189  odd2np1lem  12216  odd2np1  12217  ltoddhalfle  12237  halfleoddlt  12238  m1expo  12244  nn0enne  12246  nn0ehalf  12247  nn0o1gt2  12249  flodddiv4  12280  zeqzmulgcd  12324  gcdneg  12336  gcdaddm  12338  bezoutlemaz  12357  bezoutlembz  12358  dfgcd2  12368  gcddiv  12373  dvdssqim  12378  algcvgblem  12404  algcvga  12406  lcmneg  12429  coprmgcdb  12443  coprmdvds2  12448  qredeq  12451  divgcdcoprm0  12456  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  prmind2  12475  dvdsnprmd  12480  prmgt1  12487  nprmdvds1  12495  divgcdodd  12498  euclemma  12501  prmdvdsexpr  12505  prmfac1  12507  prmndvdsfaclt  12511  crth  12579  eulerthlemh  12586  fermltl  12589  nnnn0modprm0  12611  coprimeprodsq2  12614  pythagtriplem2  12622  pcpremul  12649  pcdvdsb  12676  pc2dvds  12686  pc11  12687  dvdsprmpweqnn  12692  dvdsprmpweqle  12693  difsqpwdvds  12694  pcfac  12706  oddprmdvds  12710  prmpwdvds  12711  1arith  12723  4sqlem11  12757  4sqlem12  12758  imasaddfnlemg  13179  erlecpbl  13197  xpsff1o  13214  imasmnd2  13317  grp1inv  13472  imasgrp2  13479  ghmpreima  13635  imasabl  13705  imasrng  13751  imasring  13859  dvdsrtr  13896  dvdsrmul1  13897  unitgrp  13911  znidomb  14453  tgtop  14573  tgidm  14579  neipsm  14659  restbasg  14673  tgrest  14674  tgcn  14713  tgcnp  14714  cnconst2  14738  cnconst  14739  cnptopresti  14743  txbasval  14772  txcnp  14776  txdis1cn  14783  bldisj  14906  xblm  14922  blssps  14932  blss  14933  blin2  14937  cnlimcim  15176  dveflem  15231  sincosq3sgn  15333  sincosq4sgn  15334  coseq0q4123  15339  ioocosf1o  15359  logbgcd1irr  15472  mpodvdsmulf1o  15495  zabsle1  15509  lgsdir2lem5  15542  lgsne0  15548  lgsdirnn0  15557  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  gausslemma2dlem2  15572  gausslemma2dlem7  15578  gausslemma2d  15579  lgseisenlem2  15581  lgsquadlem1  15587  2lgslem1a1  15596  2lgslem1b  15599  2lgslem1c  15600  2lgs  15614  2lgsoddprmlem2  15616  uzdcinzz  15771  subctctexmid  15974