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  3670  ssprsseq  3858  nlimsucg  4690  ssrelrn  4949  poltletr  5165  xp11m  5203  fvmptdf  5767  elfvmptrab1  5774  eusvobj2  6038  ovmpodf  6187  elovmporab  6256  elovmporab1w  6257  f1o2ndf1  6426  suppssdc  6462  suppssrst  6463  suppssrgst  6464  smoiso  6535  nnsseleq  6736  ecopovtrn  6868  ecopovtrng  6871  dom2lem  7013  fundmen  7049  dom1o  7071  fidifsnen  7127  findcard2  7148  findcard2s  7149  supisoex  7302  infglbti  7318  ordiso2  7328  updjud  7375  difinfsnlem  7392  enomnilem  7431  enmkvlem  7454  netap  7570  2omotaplemap  7573  cc2lem  7582  addcanpig  7651  mulcanpig  7652  addnidpig  7653  ordpipqqs  7691  ltexnqq  7725  prarloclemlo  7811  genpcdl  7836  genpcuu  7837  mulnqprl  7885  mulnqpru  7886  distrlem1prl  7899  distrlem1pru  7900  distrlem4prl  7901  distrlem4pru  7902  distrlem5prl  7903  distrlem5pru  7904  ltsopr  7913  ltexprlemfl  7926  ltexprlemfu  7928  recexprlemss1l  7952  recexprlemss1u  7953  aptiprleml  7956  ltsrprg  8064  lttrsr  8079  mulextsr1lem  8097  axapti  8346  cnegexlem1  8450  le2add  8720  lt2add  8721  ltleadd  8722  lt2sub  8736  le2sub  8737  recexre  8854  reapti  8855  apreap  8863  reapcotr  8874  remulext1  8875  apreim  8879  apcotr  8883  mulext2  8889  recexap  8929  addltmul  9477  elnnz  9589  zleloe  9626  difgtsumgt  9649  nn0n0n1ge2b  9660  nn0lt2  9662  nn0le2is012  9663  zextlt  9673  uzind2  9693  supinfneg  9930  infsupneg  9931  eluzdc  9945  qreccl  9977  elpq  9984  xltnegi  10171  xnn0lenn0nn0  10201  iccid  10261  icoshft  10326  zltaddlt1le  10344  fzofzim  10531  qbtwnxr  10621  flqeqceilz  10684  modqmuladdnn0  10734  modfzo0difsn  10761  addmodlteq  10764  frec2uzrand  10771  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  seqf1oglem1  10885  facdiv  11104  facwordi  11106  faclbnd  11107  bcpasc  11132  seq3coll  11218  fundm2domnop0  11224  fstwrdne  11267  elovmpowrd  11270  lswlgt0cl  11281  ccatrn  11301  ccatalpha  11305  swrdnd  11355  swrdswrd  11401  wrd2ind  11419  swrdccatin1  11421  pfxccatin12lem2a  11423  pfxccat3  11430  swrdccat  11431  swrdccat3blem  11435  reuccatpfxs1lem  11442  recvguniq  11684  abs00ap  11751  absext  11752  absnid  11762  cau3lem  11803  climuni  11982  2clim  11990  summodc  12073  fisumss  12082  fsumabs  12155  mertenslem2  12226  fprodssdc  12280  reeff1  12390  efieq1re  12462  dvdsmultr2  12523  dvdsleabs  12535  odd2np1lem  12562  odd2np1  12563  ltoddhalfle  12583  halfleoddlt  12584  m1expo  12590  nn0enne  12592  nn0ehalf  12593  nn0o1gt2  12595  flodddiv4  12626  zeqzmulgcd  12670  gcdneg  12682  gcdaddm  12684  bezoutlemaz  12703  bezoutlembz  12704  dfgcd2  12714  gcddiv  12719  dvdssqim  12724  algcvgblem  12750  algcvga  12752  lcmneg  12775  coprmgcdb  12789  coprmdvds2  12794  qredeq  12797  divgcdcoprm0  12802  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  prmind2  12821  dvdsnprmd  12826  prmgt1  12833  nprmdvds1  12841  divgcdodd  12844  euclemma  12847  prmdvdsexpr  12851  prmfac1  12853  prmndvdsfaclt  12857  crth  12925  eulerthlemh  12932  fermltl  12935  nnnn0modprm0  12957  coprimeprodsq2  12960  pythagtriplem2  12968  pcpremul  12995  pcdvdsb  13022  pc2dvds  13032  pc11  13033  dvdsprmpweqnn  13038  dvdsprmpweqle  13039  difsqpwdvds  13040  pcfac  13052  oddprmdvds  13056  prmpwdvds  13057  1arith  13069  4sqlem11  13103  4sqlem12  13104  imasaddfnlemg  13544  erlecpbl  13562  xpsff1o  13579  imasmnd2  13682  grp1inv  13837  imasgrp2  13844  ghmpreima  14000  imasabl  14070  imasrng  14117  imasring  14225  dvdsrtr  14263  dvdsrmul1  14264  unitgrp  14278  znidomb  14823  tgtop  14950  tgidm  14956  neipsm  15036  restbasg  15050  tgrest  15051  tgcn  15090  tgcnp  15091  cnconst2  15115  cnconst  15116  cnptopresti  15120  txbasval  15149  txcnp  15153  txdis1cn  15160  bldisj  15283  xblm  15299  blssps  15309  blss  15310  blin2  15314  cnlimcim  15553  dveflem  15608  sincosq3sgn  15710  sincosq4sgn  15711  coseq0q4123  15716  ioocosf1o  15736  logbgcd1irr  15849  pellexlem1  15862  pellexlem3  15864  mpodvdsmulf1o  15875  zabsle1  15889  lgsdir2lem5  15922  lgsne0  15928  lgsdirnn0  15937  gausslemma2dlem0i  15947  gausslemma2dlem1a  15948  gausslemma2dlem2  15952  gausslemma2dlem7  15958  gausslemma2d  15959  lgseisenlem2  15961  lgsquadlem1  15967  2lgslem1a1  15976  2lgslem1b  15979  2lgslem1c  15980  2lgs  15994  2lgsoddprmlem2  15996  upgrpredgv  16158  ausgrumgrien  16182  ausgrusgrien  16183  usgruspgrben  16198  uhgr2edg  16218  usgredg4  16227  ushgredgedg  16238  ushgredgedgloop  16240  edg0usgr  16259  uhgrspansubgrlem  16288  wlkl1loop  16370  wlk1walkdom  16371  wlklenvclwlk  16385  wlkres  16391  clwwlknonex2  16451  uzdcinzz  16587  subctctexmid  16791