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  5722  elfvmptrab1  5729  eusvobj2  5987  ovmpodf  6136  elovmporab  6205  elovmporab1w  6206  f1o2ndf1  6374  smoiso  6448  nnsseleq  6647  ecopovtrn  6779  ecopovtrng  6782  dom2lem  6923  fundmen  6959  dom1o  6977  fidifsnen  7032  findcard2  7051  findcard2s  7052  supisoex  7176  infglbti  7192  ordiso2  7202  updjud  7249  difinfsnlem  7266  enomnilem  7305  enmkvlem  7328  netap  7440  2omotaplemap  7443  cc2lem  7452  addcanpig  7521  mulcanpig  7522  addnidpig  7523  ordpipqqs  7561  ltexnqq  7595  prarloclemlo  7681  genpcdl  7706  genpcuu  7707  mulnqprl  7755  mulnqpru  7756  distrlem1prl  7769  distrlem1pru  7770  distrlem4prl  7771  distrlem4pru  7772  distrlem5prl  7773  distrlem5pru  7774  ltsopr  7783  ltexprlemfl  7796  ltexprlemfu  7798  recexprlemss1l  7822  recexprlemss1u  7823  aptiprleml  7826  ltsrprg  7934  lttrsr  7949  mulextsr1lem  7967  axapti  8217  cnegexlem1  8321  le2add  8591  lt2add  8592  ltleadd  8593  lt2sub  8607  le2sub  8608  recexre  8725  reapti  8726  apreap  8734  reapcotr  8745  remulext1  8746  apreim  8750  apcotr  8754  mulext2  8760  recexap  8800  addltmul  9348  elnnz  9456  zleloe  9493  difgtsumgt  9516  nn0n0n1ge2b  9526  nn0lt2  9528  nn0le2is012  9529  zextlt  9539  uzind2  9559  supinfneg  9790  infsupneg  9791  eluzdc  9805  qreccl  9837  elpq  9844  xltnegi  10031  xnn0lenn0nn0  10061  iccid  10121  icoshft  10186  zltaddlt1le  10203  fzofzim  10388  qbtwnxr  10477  flqeqceilz  10540  modqmuladdnn0  10590  modfzo0difsn  10617  addmodlteq  10620  frec2uzrand  10627  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  seqf1oglem1  10741  facdiv  10960  facwordi  10962  faclbnd  10963  bcpasc  10988  seq3coll  11064  fundm2domnop0  11067  fstwrdne  11110  elovmpowrd  11113  lswlgt0cl  11124  ccatrn  11144  swrdnd  11191  swrdswrd  11237  wrd2ind  11255  swrdccatin1  11257  pfxccatin12lem2a  11259  pfxccat3  11266  swrdccat  11267  swrdccat3blem  11271  reuccatpfxs1lem  11278  recvguniq  11506  abs00ap  11573  absext  11574  absnid  11584  cau3lem  11625  climuni  11804  2clim  11812  summodc  11894  fisumss  11903  fsumabs  11976  mertenslem2  12047  fprodssdc  12101  reeff1  12211  efieq1re  12283  dvdsmultr2  12344  dvdsleabs  12356  odd2np1lem  12383  odd2np1  12384  ltoddhalfle  12404  halfleoddlt  12405  m1expo  12411  nn0enne  12413  nn0ehalf  12414  nn0o1gt2  12416  flodddiv4  12447  zeqzmulgcd  12491  gcdneg  12503  gcdaddm  12505  bezoutlemaz  12524  bezoutlembz  12525  dfgcd2  12535  gcddiv  12540  dvdssqim  12545  algcvgblem  12571  algcvga  12573  lcmneg  12596  coprmgcdb  12610  coprmdvds2  12615  qredeq  12618  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  prmind2  12642  dvdsnprmd  12647  prmgt1  12654  nprmdvds1  12662  divgcdodd  12665  euclemma  12668  prmdvdsexpr  12672  prmfac1  12674  prmndvdsfaclt  12678  crth  12746  eulerthlemh  12753  fermltl  12756  nnnn0modprm0  12778  coprimeprodsq2  12781  pythagtriplem2  12789  pcpremul  12816  pcdvdsb  12843  pc2dvds  12853  pc11  12854  dvdsprmpweqnn  12859  dvdsprmpweqle  12860  difsqpwdvds  12861  pcfac  12873  oddprmdvds  12877  prmpwdvds  12878  1arith  12890  4sqlem11  12924  4sqlem12  12925  imasaddfnlemg  13347  erlecpbl  13365  xpsff1o  13382  imasmnd2  13485  grp1inv  13640  imasgrp2  13647  ghmpreima  13803  imasabl  13873  imasrng  13919  imasring  14027  dvdsrtr  14065  dvdsrmul1  14066  unitgrp  14080  znidomb  14622  tgtop  14742  tgidm  14748  neipsm  14828  restbasg  14842  tgrest  14843  tgcn  14882  tgcnp  14883  cnconst2  14907  cnconst  14908  cnptopresti  14912  txbasval  14941  txcnp  14945  txdis1cn  14952  bldisj  15075  xblm  15091  blssps  15101  blss  15102  blin2  15106  cnlimcim  15345  dveflem  15400  sincosq3sgn  15502  sincosq4sgn  15503  coseq0q4123  15508  ioocosf1o  15528  logbgcd1irr  15641  mpodvdsmulf1o  15664  zabsle1  15678  lgsdir2lem5  15711  lgsne0  15717  lgsdirnn0  15726  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem7  15747  gausslemma2d  15748  lgseisenlem2  15750  lgsquadlem1  15756  2lgslem1a1  15765  2lgslem1b  15768  2lgslem1c  15769  2lgs  15783  2lgsoddprmlem2  15785  upgrpredgv  15944  ausgrumgrien  15968  ausgrusgrien  15969  usgruspgrben  15984  uhgr2edg  16004  usgredg4  16013  ushgredgedg  16024  ushgredgedgloop  16026  wlkl1loop  16069  wlk1walkdom  16070  wlklenvclwlk  16084  uzdcinzz  16162  subctctexmid  16366