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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr4d  203  ifnebibdc  3686  ssprsseq  3877  nlimsucg  4713  ssrelrn  4972  poltletr  5188  xp11m  5226  fvmptdf  5793  elfvmptrab1  5801  eusvobj2  6071  ovmpodf  6220  elovmporab  6289  elovmporab1w  6290  f1o2ndf1  6464  suppssdc  6500  suppssrst  6501  suppssrgst  6502  smoiso  6573  nnsseleq  6774  ecopovtrn  6906  ecopovtrng  6909  dom2lem  7058  fundmen  7094  dom1o  7116  fidifsnen  7172  findcard2  7193  findcard2s  7194  supisoex  7350  infglbti  7366  ordiso2  7376  updjud  7423  difinfsnlem  7440  enomnilem  7479  enmkvlem  7502  netap  7621  2omotaplemap  7624  cc2lem  7633  addcanpig  7702  mulcanpig  7703  addnidpig  7704  ordpipqqs  7742  ltexnqq  7776  prarloclemlo  7862  genpcdl  7887  genpcuu  7888  mulnqprl  7936  mulnqpru  7937  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  distrlem5prl  7954  distrlem5pru  7955  ltsopr  7964  ltexprlemfl  7977  ltexprlemfu  7979  recexprlemss1l  8003  recexprlemss1u  8004  aptiprleml  8007  ltsrprg  8115  lttrsr  8130  mulextsr1lem  8148  axapti  8397  cnegexlem1  8503  le2add  8774  lt2add  8775  ltleadd  8776  lt2sub  8790  le2sub  8791  recexre  8909  reapti  8910  apreap  8918  reapcotr  8929  remulext1  8930  apreim  8934  apcotr  8938  mulext2  8944  recexap  8984  addltmul  9547  elnnz  9659  zleloe  9696  difgtsumgt  9719  nn0n0n1ge2b  9730  nn0lt2  9732  nn0le2is012  9733  zextlt  9743  uzind2  9763  supinfneg  10005  infsupneg  10006  eluzdc  10020  qreccl  10052  elpq  10060  xltnegi  10248  xnn0lenn0nn0  10278  iccid  10338  icoshft  10403  zltaddlt1le  10421  fzofzim  10611  qbtwnxr  10703  flqeqceilz  10770  modqmuladdnn0  10820  modfzo0difsn  10847  addmodlteq  10850  frec2uzrand  10857  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seqf1oglem1  10971  facdiv  11192  facwordi  11194  faclbnd  11195  bcpasc  11220  seq3coll  11310  fundm2domnop0  11316  fstwrdne  11359  elovmpowrd  11362  lswlgt0cl  11373  ccatrn  11393  ccatalpha  11397  swrdnd  11447  swrdswrd  11493  wrd2ind  11511  swrdccatin1  11513  pfxccatin12lem2a  11515  pfxccat3  11522  swrdccat  11523  swrdccat3blem  11527  reuccatpfxs1lem  11534  recvguniq  11777  abs00ap  11844  absext  11845  absnid  11855  cau3lem  11897  climuni  12078  2clim  12086  summodc  12169  fisumss  12178  fsumabs  12251  mertenslem2  12322  fprodssdc  12376  reeff1  12486  efieq1re  12558  dvdsmultr2  12619  dvdsleabs  12631  odd2np1lem  12658  odd2np1  12659  ltoddhalfle  12679  halfleoddlt  12680  m1expo  12686  nn0enne  12688  nn0ehalf  12689  nn0o1gt2  12691  flodddiv4  12722  zeqzmulgcd  12766  gcdneg  12778  gcdaddm  12780  bezoutlemaz  12799  bezoutlembz  12800  dfgcd2  12810  gcddiv  12815  dvdssqim  12820  algcvgblem  12846  algcvga  12848  lcmneg  12871  coprmgcdb  12885  coprmdvds2  12890  qredeq  12893  divgcdcoprm0  12898  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  prmind2  12917  dvdsnprmd  12922  prmgt1  12930  nprmdvds1  12938  divgcdodd  12941  euclemma  12944  prmdvdsexpr  12948  prmfac1  12950  prmndvdsfaclt  12954  crth  13025  eulerthlemh  13032  fermltl  13035  nnnn0modprm0  13057  coprimeprodsq2  13060  pythagtriplem2  13068  pcpremul  13095  pcdvdsb  13122  pc2dvds  13132  pc11  13133  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  difsqpwdvds  13140  pcfac  13152  oddprmdvds  13156  prmpwdvds  13157  1arith  13169  4sqlem11  13203  4sqlem12  13204  prmlem0  13243  ballotfilemfrceq  13324  imasaddfnlemg  13688  erlecpbl  13706  xpsff1o  13723  imasmnd2  13812  grp1inv  13965  imasgrp2  13966  ghmpreima  14122  imasabl  14224  imasrng  14339  imasring  14453  dvdsrtr  14492  dvdsrmul1  14493  unitgrp  14507  znidomb  15077  tgtop  15260  tgidm  15266  neipsm  15346  restbasg  15360  tgrest  15361  tgcn  15400  tgcnp  15401  cnconst2  15425  cnconst  15426  cnptopresti  15430  txbasval  15459  txcnp  15463  txdis1cn  15470  bldisj  15593  xblm  15609  blssps  15619  blss  15620  blin2  15624  cnlimcim  15863  dveflem  15918  sincosq3sgn  16021  sincosq4sgn  16022  coseq0q4123  16027  ioocosf1o  16047  logbgcd1irr  16164  birthdaylem1g  16186  pellexlem1  16190  pellexlem3  16192  mpodvdsmulf1o  16245  ppiublem1  16252  chtqub  16257  bclbnd  16268  bposlem1  16272  bposlem5  16276  zabsle1  16284  lgsdir2lem5  16317  lgsne0  16323  lgsdirnn0  16332  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  gausslemma2dlem2  16347  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem2  16356  lgsquadlem1  16362  2lgslem1a1  16371  2lgslem1b  16374  2lgslem1c  16375  2lgs  16389  2lgsoddprmlem2  16391  upgrpredgv  16553  ausgrumgrien  16577  ausgrusgrien  16578  usgruspgrben  16593  uhgr2edg  16613  usgredg4  16622  ushgredgedg  16633  ushgredgedgloop  16635  edg0usgr  16654  uhgrspansubgrlem  16683  wlkl1loop  16765  wlk1walkdom  16766  wlklenvclwlk  16780  wlkres  16786  clwwlknonex2  16846  uzdcinzz  16992  subctctexmid  17196