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  3686  ssprsseq  3875  nlimsucg  4711  ssrelrn  4970  poltletr  5186  xp11m  5224  fvmptdf  5790  elfvmptrab1  5797  eusvobj2  6064  ovmpodf  6213  elovmporab  6282  elovmporab1w  6283  f1o2ndf1  6457  suppssdc  6493  suppssrst  6494  suppssrgst  6495  smoiso  6566  nnsseleq  6767  ecopovtrn  6899  ecopovtrng  6902  dom2lem  7051  fundmen  7087  dom1o  7109  fidifsnen  7165  findcard2  7186  findcard2s  7187  supisoex  7342  infglbti  7358  ordiso2  7368  updjud  7415  difinfsnlem  7432  enomnilem  7471  enmkvlem  7494  netap  7613  2omotaplemap  7616  cc2lem  7625  addcanpig  7694  mulcanpig  7695  addnidpig  7696  ordpipqqs  7734  ltexnqq  7768  prarloclemlo  7854  genpcdl  7879  genpcuu  7880  mulnqprl  7928  mulnqpru  7929  distrlem1prl  7942  distrlem1pru  7943  distrlem4prl  7944  distrlem4pru  7945  distrlem5prl  7946  distrlem5pru  7947  ltsopr  7956  ltexprlemfl  7969  ltexprlemfu  7971  recexprlemss1l  7995  recexprlemss1u  7996  aptiprleml  7999  ltsrprg  8107  lttrsr  8122  mulextsr1lem  8140  axapti  8389  cnegexlem1  8494  le2add  8765  lt2add  8766  ltleadd  8767  lt2sub  8781  le2sub  8782  recexre  8899  reapti  8900  apreap  8908  reapcotr  8919  remulext1  8920  apreim  8924  apcotr  8928  mulext2  8934  recexap  8974  addltmul  9524  elnnz  9636  zleloe  9673  difgtsumgt  9696  nn0n0n1ge2b  9707  nn0lt2  9709  nn0le2is012  9710  zextlt  9720  uzind2  9740  supinfneg  9977  infsupneg  9978  eluzdc  9992  qreccl  10024  elpq  10031  xltnegi  10219  xnn0lenn0nn0  10249  iccid  10309  icoshft  10374  zltaddlt1le  10392  fzofzim  10581  qbtwnxr  10673  flqeqceilz  10736  modqmuladdnn0  10786  modfzo0difsn  10813  addmodlteq  10816  frec2uzrand  10823  frecuzrdgtcl  10830  frecuzrdgfunlem  10837  seqf1oglem1  10937  facdiv  11157  facwordi  11159  faclbnd  11160  bcpasc  11185  seq3coll  11275  fundm2domnop0  11281  fstwrdne  11324  elovmpowrd  11327  lswlgt0cl  11338  ccatrn  11358  ccatalpha  11362  swrdnd  11412  swrdswrd  11458  wrd2ind  11476  swrdccatin1  11478  pfxccatin12lem2a  11480  pfxccat3  11487  swrdccat  11488  swrdccat3blem  11492  reuccatpfxs1lem  11499  recvguniq  11742  abs00ap  11809  absext  11810  absnid  11820  cau3lem  11861  climuni  12040  2clim  12048  summodc  12131  fisumss  12140  fsumabs  12213  mertenslem2  12284  fprodssdc  12338  reeff1  12448  efieq1re  12520  dvdsmultr2  12581  dvdsleabs  12593  odd2np1lem  12620  odd2np1  12621  ltoddhalfle  12641  halfleoddlt  12642  m1expo  12648  nn0enne  12650  nn0ehalf  12651  nn0o1gt2  12653  flodddiv4  12684  zeqzmulgcd  12728  gcdneg  12740  gcdaddm  12742  bezoutlemaz  12761  bezoutlembz  12762  dfgcd2  12772  gcddiv  12777  dvdssqim  12782  algcvgblem  12808  algcvga  12810  lcmneg  12833  coprmgcdb  12847  coprmdvds2  12852  qredeq  12855  divgcdcoprm0  12860  divgcdcoprmex  12861  cncongr1  12862  cncongr2  12863  prmind2  12879  dvdsnprmd  12884  prmgt1  12891  nprmdvds1  12899  divgcdodd  12902  euclemma  12905  prmdvdsexpr  12909  prmfac1  12911  prmndvdsfaclt  12915  crth  12983  eulerthlemh  12990  fermltl  12993  nnnn0modprm0  13015  coprimeprodsq2  13018  pythagtriplem2  13026  pcpremul  13053  pcdvdsb  13080  pc2dvds  13090  pc11  13091  dvdsprmpweqnn  13096  dvdsprmpweqle  13097  difsqpwdvds  13098  pcfac  13110  oddprmdvds  13114  prmpwdvds  13115  1arith  13127  4sqlem11  13161  4sqlem12  13162  ballotfilemfrceq  13253  imasaddfnlemg  13615  erlecpbl  13633  xpsff1o  13650  imasmnd2  13739  grp1inv  13892  imasgrp2  13893  ghmpreima  14049  imasabl  14120  imasrng  14233  imasring  14345  dvdsrtr  14384  dvdsrmul1  14385  unitgrp  14399  znidomb  14968  tgtop  15095  tgidm  15101  neipsm  15181  restbasg  15195  tgrest  15196  tgcn  15235  tgcnp  15236  cnconst2  15260  cnconst  15261  cnptopresti  15265  txbasval  15294  txcnp  15298  txdis1cn  15305  bldisj  15428  xblm  15444  blssps  15454  blss  15455  blin2  15459  cnlimcim  15698  dveflem  15753  sincosq3sgn  15855  sincosq4sgn  15856  coseq0q4123  15861  ioocosf1o  15881  logbgcd1irr  15995  pellexlem1  16008  pellexlem3  16010  mpodvdsmulf1o  16021  zabsle1  16035  lgsdir2lem5  16068  lgsne0  16074  lgsdirnn0  16083  gausslemma2dlem0i  16093  gausslemma2dlem1a  16094  gausslemma2dlem2  16098  gausslemma2dlem7  16104  gausslemma2d  16105  lgseisenlem2  16107  lgsquadlem1  16113  2lgslem1a1  16122  2lgslem1b  16125  2lgslem1c  16126  2lgs  16140  2lgsoddprmlem2  16142  upgrpredgv  16304  ausgrumgrien  16328  ausgrusgrien  16329  usgruspgrben  16344  uhgr2edg  16364  usgredg4  16373  ushgredgedg  16384  ushgredgedgloop  16386  edg0usgr  16405  uhgrspansubgrlem  16434  wlkl1loop  16516  wlk1walkdom  16517  wlklenvclwlk  16531  wlkres  16537  clwwlknonex2  16597  uzdcinzz  16743  subctctexmid  16947