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  3652  ssprsseq  3836  nlimsucg  4666  ssrelrn  4924  poltletr  5139  xp11m  5177  fvmptdf  5737  elfvmptrab1  5744  eusvobj2  6009  ovmpodf  6158  elovmporab  6227  elovmporab1w  6228  f1o2ndf1  6398  smoiso  6473  nnsseleq  6674  ecopovtrn  6806  ecopovtrng  6809  dom2lem  6950  fundmen  6986  dom1o  7007  fidifsnen  7062  findcard2  7083  findcard2s  7084  supisoex  7213  infglbti  7229  ordiso2  7239  updjud  7286  difinfsnlem  7303  enomnilem  7342  enmkvlem  7365  netap  7478  2omotaplemap  7481  cc2lem  7490  addcanpig  7559  mulcanpig  7560  addnidpig  7561  ordpipqqs  7599  ltexnqq  7633  prarloclemlo  7719  genpcdl  7744  genpcuu  7745  mulnqprl  7793  mulnqpru  7794  distrlem1prl  7807  distrlem1pru  7808  distrlem4prl  7809  distrlem4pru  7810  distrlem5prl  7811  distrlem5pru  7812  ltsopr  7821  ltexprlemfl  7834  ltexprlemfu  7836  recexprlemss1l  7860  recexprlemss1u  7861  aptiprleml  7864  ltsrprg  7972  lttrsr  7987  mulextsr1lem  8005  axapti  8255  cnegexlem1  8359  le2add  8629  lt2add  8630  ltleadd  8631  lt2sub  8645  le2sub  8646  recexre  8763  reapti  8764  apreap  8772  reapcotr  8783  remulext1  8784  apreim  8788  apcotr  8792  mulext2  8798  recexap  8838  addltmul  9386  elnnz  9494  zleloe  9531  difgtsumgt  9554  nn0n0n1ge2b  9564  nn0lt2  9566  nn0le2is012  9567  zextlt  9577  uzind2  9597  supinfneg  9834  infsupneg  9835  eluzdc  9849  qreccl  9881  elpq  9888  xltnegi  10075  xnn0lenn0nn0  10105  iccid  10165  icoshft  10230  zltaddlt1le  10247  fzofzim  10433  qbtwnxr  10523  flqeqceilz  10586  modqmuladdnn0  10636  modfzo0difsn  10663  addmodlteq  10666  frec2uzrand  10673  frecuzrdgtcl  10680  frecuzrdgfunlem  10687  seqf1oglem1  10787  facdiv  11006  facwordi  11008  faclbnd  11009  bcpasc  11034  seq3coll  11112  fundm2domnop0  11118  fstwrdne  11161  elovmpowrd  11164  lswlgt0cl  11175  ccatrn  11195  ccatalpha  11199  swrdnd  11249  swrdswrd  11295  wrd2ind  11313  swrdccatin1  11315  pfxccatin12lem2a  11317  pfxccat3  11324  swrdccat  11325  swrdccat3blem  11329  reuccatpfxs1lem  11336  recvguniq  11578  abs00ap  11645  absext  11646  absnid  11656  cau3lem  11697  climuni  11876  2clim  11884  summodc  11967  fisumss  11976  fsumabs  12049  mertenslem2  12120  fprodssdc  12174  reeff1  12284  efieq1re  12356  dvdsmultr2  12417  dvdsleabs  12429  odd2np1lem  12456  odd2np1  12457  ltoddhalfle  12477  halfleoddlt  12478  m1expo  12484  nn0enne  12486  nn0ehalf  12487  nn0o1gt2  12489  flodddiv4  12520  zeqzmulgcd  12564  gcdneg  12576  gcdaddm  12578  bezoutlemaz  12597  bezoutlembz  12598  dfgcd2  12608  gcddiv  12613  dvdssqim  12618  algcvgblem  12644  algcvga  12646  lcmneg  12669  coprmgcdb  12683  coprmdvds2  12688  qredeq  12691  divgcdcoprm0  12696  divgcdcoprmex  12697  cncongr1  12698  cncongr2  12699  prmind2  12715  dvdsnprmd  12720  prmgt1  12727  nprmdvds1  12735  divgcdodd  12738  euclemma  12741  prmdvdsexpr  12745  prmfac1  12747  prmndvdsfaclt  12751  crth  12819  eulerthlemh  12826  fermltl  12829  nnnn0modprm0  12851  coprimeprodsq2  12854  pythagtriplem2  12862  pcpremul  12889  pcdvdsb  12916  pc2dvds  12926  pc11  12927  dvdsprmpweqnn  12932  dvdsprmpweqle  12933  difsqpwdvds  12934  pcfac  12946  oddprmdvds  12950  prmpwdvds  12951  1arith  12963  4sqlem11  12997  4sqlem12  12998  imasaddfnlemg  13420  erlecpbl  13438  xpsff1o  13455  imasmnd2  13558  grp1inv  13713  imasgrp2  13720  ghmpreima  13876  imasabl  13946  imasrng  13993  imasring  14101  dvdsrtr  14139  dvdsrmul1  14140  unitgrp  14154  znidomb  14696  tgtop  14821  tgidm  14827  neipsm  14907  restbasg  14921  tgrest  14922  tgcn  14961  tgcnp  14962  cnconst2  14986  cnconst  14987  cnptopresti  14991  txbasval  15020  txcnp  15024  txdis1cn  15031  bldisj  15154  xblm  15170  blssps  15180  blss  15181  blin2  15185  cnlimcim  15424  dveflem  15479  sincosq3sgn  15581  sincosq4sgn  15582  coseq0q4123  15587  ioocosf1o  15607  logbgcd1irr  15720  mpodvdsmulf1o  15743  zabsle1  15757  lgsdir2lem5  15790  lgsne0  15796  lgsdirnn0  15805  gausslemma2dlem0i  15815  gausslemma2dlem1a  15816  gausslemma2dlem2  15820  gausslemma2dlem7  15826  gausslemma2d  15827  lgseisenlem2  15829  lgsquadlem1  15835  2lgslem1a1  15844  2lgslem1b  15847  2lgslem1c  15848  2lgs  15862  2lgsoddprmlem2  15864  upgrpredgv  16026  ausgrumgrien  16050  ausgrusgrien  16051  usgruspgrben  16066  uhgr2edg  16086  usgredg4  16095  ushgredgedg  16106  ushgredgedgloop  16108  edg0usgr  16127  uhgrspansubgrlem  16156  wlkl1loop  16238  wlk1walkdom  16239  wlklenvclwlk  16253  wlkres  16259  clwwlknonex2  16319  uzdcinzz  16455  subctctexmid  16661