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  3651  ssprsseq  3835  nlimsucg  4664  ssrelrn  4922  poltletr  5137  xp11m  5175  fvmptdf  5734  elfvmptrab1  5741  eusvobj2  6004  ovmpodf  6153  elovmporab  6222  elovmporab1w  6223  f1o2ndf1  6393  smoiso  6468  nnsseleq  6669  ecopovtrn  6801  ecopovtrng  6804  dom2lem  6945  fundmen  6981  dom1o  7002  fidifsnen  7057  findcard2  7078  findcard2s  7079  supisoex  7208  infglbti  7224  ordiso2  7234  updjud  7281  difinfsnlem  7298  enomnilem  7337  enmkvlem  7360  netap  7473  2omotaplemap  7476  cc2lem  7485  addcanpig  7554  mulcanpig  7555  addnidpig  7556  ordpipqqs  7594  ltexnqq  7628  prarloclemlo  7714  genpcdl  7739  genpcuu  7740  mulnqprl  7788  mulnqpru  7789  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  distrlem5prl  7806  distrlem5pru  7807  ltsopr  7816  ltexprlemfl  7829  ltexprlemfu  7831  recexprlemss1l  7855  recexprlemss1u  7856  aptiprleml  7859  ltsrprg  7967  lttrsr  7982  mulextsr1lem  8000  axapti  8250  cnegexlem1  8354  le2add  8624  lt2add  8625  ltleadd  8626  lt2sub  8640  le2sub  8641  recexre  8758  reapti  8759  apreap  8767  reapcotr  8778  remulext1  8779  apreim  8783  apcotr  8787  mulext2  8793  recexap  8833  addltmul  9381  elnnz  9489  zleloe  9526  difgtsumgt  9549  nn0n0n1ge2b  9559  nn0lt2  9561  nn0le2is012  9562  zextlt  9572  uzind2  9592  supinfneg  9829  infsupneg  9830  eluzdc  9844  qreccl  9876  elpq  9883  xltnegi  10070  xnn0lenn0nn0  10100  iccid  10160  icoshft  10225  zltaddlt1le  10242  fzofzim  10428  qbtwnxr  10518  flqeqceilz  10581  modqmuladdnn0  10631  modfzo0difsn  10658  addmodlteq  10661  frec2uzrand  10668  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1oglem1  10782  facdiv  11001  facwordi  11003  faclbnd  11004  bcpasc  11029  seq3coll  11107  fundm2domnop0  11113  fstwrdne  11156  elovmpowrd  11159  lswlgt0cl  11170  ccatrn  11190  ccatalpha  11194  swrdnd  11244  swrdswrd  11290  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem2a  11312  pfxccat3  11319  swrdccat  11320  swrdccat3blem  11324  reuccatpfxs1lem  11331  recvguniq  11573  abs00ap  11640  absext  11641  absnid  11651  cau3lem  11692  climuni  11871  2clim  11879  summodc  11962  fisumss  11971  fsumabs  12044  mertenslem2  12115  fprodssdc  12169  reeff1  12279  efieq1re  12351  dvdsmultr2  12412  dvdsleabs  12424  odd2np1lem  12451  odd2np1  12452  ltoddhalfle  12472  halfleoddlt  12473  m1expo  12479  nn0enne  12481  nn0ehalf  12482  nn0o1gt2  12484  flodddiv4  12515  zeqzmulgcd  12559  gcdneg  12571  gcdaddm  12573  bezoutlemaz  12592  bezoutlembz  12593  dfgcd2  12603  gcddiv  12608  dvdssqim  12613  algcvgblem  12639  algcvga  12641  lcmneg  12664  coprmgcdb  12678  coprmdvds2  12683  qredeq  12686  divgcdcoprm0  12691  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  prmind2  12710  dvdsnprmd  12715  prmgt1  12722  nprmdvds1  12730  divgcdodd  12733  euclemma  12736  prmdvdsexpr  12740  prmfac1  12742  prmndvdsfaclt  12746  crth  12814  eulerthlemh  12821  fermltl  12824  nnnn0modprm0  12846  coprimeprodsq2  12849  pythagtriplem2  12857  pcpremul  12884  pcdvdsb  12911  pc2dvds  12921  pc11  12922  dvdsprmpweqnn  12927  dvdsprmpweqle  12928  difsqpwdvds  12929  pcfac  12941  oddprmdvds  12945  prmpwdvds  12946  1arith  12958  4sqlem11  12992  4sqlem12  12993  imasaddfnlemg  13415  erlecpbl  13433  xpsff1o  13450  imasmnd2  13553  grp1inv  13708  imasgrp2  13715  ghmpreima  13871  imasabl  13941  imasrng  13988  imasring  14096  dvdsrtr  14134  dvdsrmul1  14135  unitgrp  14149  znidomb  14691  tgtop  14811  tgidm  14817  neipsm  14897  restbasg  14911  tgrest  14912  tgcn  14951  tgcnp  14952  cnconst2  14976  cnconst  14977  cnptopresti  14981  txbasval  15010  txcnp  15014  txdis1cn  15021  bldisj  15144  xblm  15160  blssps  15170  blss  15171  blin2  15175  cnlimcim  15414  dveflem  15469  sincosq3sgn  15571  sincosq4sgn  15572  coseq0q4123  15577  ioocosf1o  15597  logbgcd1irr  15710  mpodvdsmulf1o  15733  zabsle1  15747  lgsdir2lem5  15780  lgsne0  15786  lgsdirnn0  15795  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem2  15819  lgsquadlem1  15825  2lgslem1a1  15834  2lgslem1b  15837  2lgslem1c  15838  2lgs  15852  2lgsoddprmlem2  15854  upgrpredgv  16016  ausgrumgrien  16040  ausgrusgrien  16041  usgruspgrben  16056  uhgr2edg  16076  usgredg4  16085  ushgredgedg  16096  ushgredgedgloop  16098  edg0usgr  16117  uhgrspansubgrlem  16146  wlkl1loop  16228  wlk1walkdom  16229  wlklenvclwlk  16243  wlkres  16249  clwwlknonex2  16309  uzdcinzz  16445  subctctexmid  16652