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  3648  ssprsseq  3830  nlimsucg  4658  ssrelrn  4914  poltletr  5129  xp11m  5167  fvmptdf  5724  elfvmptrab1  5731  eusvobj2  5993  ovmpodf  6142  elovmporab  6211  elovmporab1w  6212  f1o2ndf1  6380  smoiso  6454  nnsseleq  6655  ecopovtrn  6787  ecopovtrng  6790  dom2lem  6931  fundmen  6967  dom1o  6985  fidifsnen  7040  findcard2  7059  findcard2s  7060  supisoex  7187  infglbti  7203  ordiso2  7213  updjud  7260  difinfsnlem  7277  enomnilem  7316  enmkvlem  7339  netap  7451  2omotaplemap  7454  cc2lem  7463  addcanpig  7532  mulcanpig  7533  addnidpig  7534  ordpipqqs  7572  ltexnqq  7606  prarloclemlo  7692  genpcdl  7717  genpcuu  7718  mulnqprl  7766  mulnqpru  7767  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  distrlem5prl  7784  distrlem5pru  7785  ltsopr  7794  ltexprlemfl  7807  ltexprlemfu  7809  recexprlemss1l  7833  recexprlemss1u  7834  aptiprleml  7837  ltsrprg  7945  lttrsr  7960  mulextsr1lem  7978  axapti  8228  cnegexlem1  8332  le2add  8602  lt2add  8603  ltleadd  8604  lt2sub  8618  le2sub  8619  recexre  8736  reapti  8737  apreap  8745  reapcotr  8756  remulext1  8757  apreim  8761  apcotr  8765  mulext2  8771  recexap  8811  addltmul  9359  elnnz  9467  zleloe  9504  difgtsumgt  9527  nn0n0n1ge2b  9537  nn0lt2  9539  nn0le2is012  9540  zextlt  9550  uzind2  9570  supinfneg  9802  infsupneg  9803  eluzdc  9817  qreccl  9849  elpq  9856  xltnegi  10043  xnn0lenn0nn0  10073  iccid  10133  icoshft  10198  zltaddlt1le  10215  fzofzim  10400  qbtwnxr  10489  flqeqceilz  10552  modqmuladdnn0  10602  modfzo0difsn  10629  addmodlteq  10632  frec2uzrand  10639  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqf1oglem1  10753  facdiv  10972  facwordi  10974  faclbnd  10975  bcpasc  11000  seq3coll  11077  fundm2domnop0  11080  fstwrdne  11123  elovmpowrd  11126  lswlgt0cl  11137  ccatrn  11157  ccatalpha  11161  swrdnd  11207  swrdswrd  11253  wrd2ind  11271  swrdccatin1  11273  pfxccatin12lem2a  11275  pfxccat3  11282  swrdccat  11283  swrdccat3blem  11287  reuccatpfxs1lem  11294  recvguniq  11522  abs00ap  11589  absext  11590  absnid  11600  cau3lem  11641  climuni  11820  2clim  11828  summodc  11910  fisumss  11919  fsumabs  11992  mertenslem2  12063  fprodssdc  12117  reeff1  12227  efieq1re  12299  dvdsmultr2  12360  dvdsleabs  12372  odd2np1lem  12399  odd2np1  12400  ltoddhalfle  12420  halfleoddlt  12421  m1expo  12427  nn0enne  12429  nn0ehalf  12430  nn0o1gt2  12432  flodddiv4  12463  zeqzmulgcd  12507  gcdneg  12519  gcdaddm  12521  bezoutlemaz  12540  bezoutlembz  12541  dfgcd2  12551  gcddiv  12556  dvdssqim  12561  algcvgblem  12587  algcvga  12589  lcmneg  12612  coprmgcdb  12626  coprmdvds2  12631  qredeq  12634  divgcdcoprm0  12639  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  prmind2  12658  dvdsnprmd  12663  prmgt1  12670  nprmdvds1  12678  divgcdodd  12681  euclemma  12684  prmdvdsexpr  12688  prmfac1  12690  prmndvdsfaclt  12694  crth  12762  eulerthlemh  12769  fermltl  12772  nnnn0modprm0  12794  coprimeprodsq2  12797  pythagtriplem2  12805  pcpremul  12832  pcdvdsb  12859  pc2dvds  12869  pc11  12870  dvdsprmpweqnn  12875  dvdsprmpweqle  12876  difsqpwdvds  12877  pcfac  12889  oddprmdvds  12893  prmpwdvds  12894  1arith  12906  4sqlem11  12940  4sqlem12  12941  imasaddfnlemg  13363  erlecpbl  13381  xpsff1o  13398  imasmnd2  13501  grp1inv  13656  imasgrp2  13663  ghmpreima  13819  imasabl  13889  imasrng  13935  imasring  14043  dvdsrtr  14081  dvdsrmul1  14082  unitgrp  14096  znidomb  14638  tgtop  14758  tgidm  14764  neipsm  14844  restbasg  14858  tgrest  14859  tgcn  14898  tgcnp  14899  cnconst2  14923  cnconst  14924  cnptopresti  14928  txbasval  14957  txcnp  14961  txdis1cn  14968  bldisj  15091  xblm  15107  blssps  15117  blss  15118  blin2  15122  cnlimcim  15361  dveflem  15416  sincosq3sgn  15518  sincosq4sgn  15519  coseq0q4123  15524  ioocosf1o  15544  logbgcd1irr  15657  mpodvdsmulf1o  15680  zabsle1  15694  lgsdir2lem5  15727  lgsne0  15733  lgsdirnn0  15742  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2dlem2  15757  gausslemma2dlem7  15763  gausslemma2d  15764  lgseisenlem2  15766  lgsquadlem1  15772  2lgslem1a1  15781  2lgslem1b  15784  2lgslem1c  15785  2lgs  15799  2lgsoddprmlem2  15801  upgrpredgv  15960  ausgrumgrien  15984  ausgrusgrien  15985  usgruspgrben  16000  uhgr2edg  16020  usgredg4  16029  ushgredgedg  16040  ushgredgedgloop  16042  wlkl1loop  16104  wlk1walkdom  16105  wlklenvclwlk  16119  wlkres  16123  uzdcinzz  16245  subctctexmid  16453