Theorem sylanc 473

Description: A syllogism inference combined with contraction.

Hypotheses

Ref	Expression
sylanc.1	|- ((ph /\ ps) -> ch)
sylanc.2	|- (th -> ph)
sylanc.3	|- (th -> ps)

Assertion

Ref	Expression
sylanc	|- (th -> ch)

Proof of Theorem sylanc

Step	Hyp	Ref	Expression
1		sylanc.1	. . 3 |- ((ph /\ ps) -> ch)
2	1	ex 371	. 2 |- (ph -> (ps -> ch))
3		sylanc.2	. 2 |- (th -> ph)
4		sylanc.3	. 2 |- (th -> ps)
5	2, 3, 4	sylc 68	1 |- (th -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  sylancr 474  syl2anc 475  sylancom 478  anim12d 561  orim12d 568  pm5.21ni 682  ax11indalem 1407  ax11inda2ALT 1408  eueq2 1964  eueq3 1965  sbc2or 2006  sstrd 2126  ralidm 2411  raaan 2414  sspr 2540  exss 2847  ordelord 2997  onfr 3014  reuuniss 3112  reuuniss2 3114  reuunixfr 3129  onnmin 3160  onminex 3164  onmindif2 3169  ordunel 3181  limsssuc 3204  peano5 3241  unixp 3622  cnvexg 3624  cnvpo 3627  cofunexg 3686  funfni 3694  fnresdm 3702  fnex 3713  fconstg 3766  f1ores 3811  resdif 3816  fimacnv 3924  dff3 3931  fconst3 3964  f1ocnvfv3 3997  oprabex2g 4080  sbcopeq1a 4171  csbopeq1a 4172  dfoprab5s 4177  1stconst 4190  2ndconst 4191  tfrlem10 4221  tfrlem12 4223  oesuc 4302  odi 4346  oewordri 4355  oeworde 4356  oelim2 4358  en2d 4541  undom 4579  xpdom1 4584  ac6sfilem3 4590  ac6sfi 4591  sbthlem8 4599  2pwuninel 4632  2pwne 4634  limenpsi 4652  limensuci 4653  php3 4662  unblem4 4689  unbnn 4690  unifi 4701  fodomfi 4709  iunfi 4712  pwfilem 4713  supub 4723  suplub 4724  supmax 4732  suppr 4733  noinfep 4786  r1ord 4801  rankr1 4820  rankxplim3 4860  fodom 4944  unidom 4954  uniimadom 4956  unxpdomlem 4993  unxpdom2 4995  cardalephex 5036  alephval2 5052  alephval3 5053  cfsuc 5065  cdafi 5088  nnaun 5091  axrepnd 5100  indpi 5188  halfpq 5236  ltaddpr 5294  ltexprlem2 5297  negexsr 5365  mulgt0sr 5368  axmulopr 5420  axcnre 5440  cnegex 5502  nnncan1 5621  mulsub 5631  pm2.61ltlei 5688  lecasei 5775  posdif 5808  recextlem2 5839  recex 5840  muleqadd 5852  divcan2 5873  recid2 5882  divrec2 5886  div23 5888  divsubdir 5914  divdivdiv 5924  divcan6 5930  conjmul 5937  lemul1 5973  lemul1OLD 5974  lemul2aOLD 5984  ltmul12a 5985  lemul12aOLD 5987  lediv1 5995  lt2mul2divOLD 6017  lemuldiv 6020  lt2msqi 6026  lediv2 6036  lediv12a 6041  lediv2a 6042  recp1lt1 6046  recreclt 6047  ledivp1 6050  ledivp1i 6051  ltdivp1i 6052  nnge1 6088  nngt1ne1 6089  nndivtr 6106  halfaddsub 6187  lt2halves 6188  avgle 6190  lbinfm 6216  infm3lem 6221  suprub 6224  infmrcl 6237  nnrecl 6240  xrub 6248  supxrre 6251  supxrunb1 6257  supxrbnd 6259  supxrub 6266  nn0ltp1le 6295  zltp1le 6349  z2ge 6359  gtndiv 6364  zindd 6386  qaddcl 6408  qmulcl 6410  qbtwnxr 6419  flid 6433  flval2 6437  flval3 6438  flbi2 6440  fladdz 6443  flhalf 6446  quoremz 6451  quoremnn0ALT 6452  quoremnn0 6453  intfrac2 6454  intfracq 6455  fldiv 6456  modcl 6461  modge0 6462  modlt 6463  flmod 6465  intfrac 6466  flmulnn0 6467  flmulnn0OLD 6468  modmulnn 6469  zmodcl 6470  modid 6471  modabs 6473  modcyc 6475  modadd1 6477  modmul1 6478  moddi 6479  modsubdir 6480  modirr 6481  iooin 6498  iccsupr 6525  icoshft 6535  icoshftf1oii 6536  uzneg 6556  uzind4 6577  infmssuzcl 6594  eluzfz1 6615  eluzfz2 6617  fzen 6622  fznn0sub2 6629  fzelp1 6639  elfzp1 6641  fzrev2i 6644  fzrev3 6645  fzneuz 6649  fsequb 6654  fsequb2 6655  fseqsupubi 6657  cardfz 6671  seq1lem2 6675  ser1monoi 6702  shftval2 6712  shftval5 6715  2shfti 6717  shftcan2 6718  seqzp1 6743  seqzfveq 6749  seqzres 6755  seqzres2 6756  expeq0 6780  expgt0 6783  mulexp 6788  exprec 6789  exprecOLD 6790  expadd 6791  expsub 6793  expsubOLD 6794  expm1 6795  expordi 6797  expwordi 6800  expord2 6801  expmwordi 6803  exple1 6804  expubnd 6805  sqlecan 6838  subsq 6839  bernneq 6849  bernneqOLD 6850  expnbnd 6852  expnlbnd 6853  expnlbnd2 6854  digit2 6855  digit1 6856  rpsqrcl 6916  cjcl 6965  imre 6974  reim0 6975  mulre 6978  cjexp 7018  recj 7019  imcj 7020  cj11OLD 7032  abscl 7035  absvalsq 7037  absreim 7059  absdivzi 7061  absexp 7070  sqabs 7071  absrele 7072  absimle 7073  recvalzi 7090  cjdivi 7091  absidm 7095  abssubge0 7098  abs3dif 7102  abs2difabs 7106  seq1ubi 7115  cvg2i 7125  caubndi 7129  ser1absdiflem 7132  ser1absdifi 7133  faclbnd 7148  faclbnd2 7149  faclbnd3 7150  faclbnd4lem3 7153  faclbnd5 7156  faclbnd6 7157  facavg 7158  bcval2 7162  bccmpl 7165  bcn0 7166  bcnp11 7168  bcnp1n 7169  bccl2 7174  bccl 7175  permnn 7176  dffsum 7201  fsump1s 7216  fsumcllem 7217  fsumsplit 7223  fsumadd 7225  fsumcom 7231  fsumrev 7232  fsumrev2 7233  fsumshft 7234  fsummulc1 7236  fsumdivcALT 7239  fsum0 7242  fsumcmp 7243  fsumcmpndx2 7245  fsumabs 7246  serz1p 7255  serzrelem 7264  binomlem1 7269  binomlem2 7270  binomlem4 7272  binomlem5 7273  bcxmas 7279  clm4lei 7284  2climnn 7305  2climnn0 7306  climrecl 7313  climge0 7315  climaddlem3 7319  climaddc1 7321  climmullem1 7323  climmullem2 7324  climmullem3 7325  climmullem4 7326  climmullem5 7327  climmullem8 7330  climmulc2 7332  climsub 7333  climsubc2 7334  climcmplem 7340  clim2serzi 7348  climserzlei 7350  climcji 7353  climubii 7356  climsupi 7358  caucvglem6 7365  caucvgi 7366  serzf0i 7372  ser1cmpi 7377  ser1cmp2i 7380  cvgcmp2lem 7383  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  isum1p 7410  iserzgt0 7415  isummulc1iALT 7417  reccnv 7422  infcvglem1 7425  infcvglem3 7427  arisumi 7430  explecnv 7438  geoseri 7439  georeclim 7445  geoisumr 7448  0.999... 7451  cvgratlem2ALT 7453  cvgratlem1 7455  cvgratlem2 7456  cvgratlem4 7458  cvgratlem5 7459  fsum0diaglem1 7461  fsum0diaglem2 7462  fsum0diag2 7464  elcncf1di 7475  cjcncf 7483  ivthlem6 7491  ivthlem7 7492  efcltlem1 7509  efcltlem2 7510  ef0lem 7515  efseq0ex 7516  erelem1 7524  erelem3 7526  efaddlem3 7545  efaddlem5 7547  efaddlem6 7548  efaddlem10 7552  efaddlem15 7557  efaddlem16 7558  efaddlem17 7559  efaddlem18 7560  efaddlem19 7561  efaddlem23 7565  efaddlem25 7567  efaddlem27 7569  eff2 7575  efsub 7576  efexp 7577  eftabsi 7580  ef1tllem 7586  ef01tllem1 7588  ef01tllem2 7589  ef01tllem2OLD 7590  eirrlem4 7597  abspef01tlubi 7603  efgt1i 7611  absefm1lei 7620  eflegeolem1 7621  efcnlem2 7628  efcn 7631  reeff1o 7634  efi4p 7643  resin4p 7644  recos4p 7645  sinneg 7650  cosneg 7651  efival 7655  efmival 7656  efeul 7657  sinsub 7663  cossub 7664  addsin 7665  subcos 7668  sincossq 7669  sin2t 7670  cos2t 7671  cos2tsin 7672  sinbnd 7674  cosbnd 7675  sin01bndlem2 7677  sin01bndlem3 7678  cos01bndlem2 7679  cos01bndlem3 7680  sin01gt0 7685  cos01gt0 7686  sin02gt0 7687  absefi 7691  absef 7692  absefib 7693  efieq1re 7694  demoivre 7695  acdc3lem 7697  acdc2lem2 7701  acdc5lem2 7704  acdclem 7706  acdcALT 7708  znnenlem 7713  unbenlem 7716  infpnlem2 7719  ruclem4 7725  ruclem13 7734  infxpidmlem1 7764  infxpidmlem11 7774  infxpidmlem12 7775  infunabs 7777  infcdaabs 7778  infcda 7779  infdif 7780  infxp 7784  alephexp1 7796  alephsuc3 7797  tgval3 7837  topbas 7839  basgen2 7851  ntrval 7886  clsval 7887  clsss 7897  elcls 7914  clsndisj 7916  neival 7927  neiss 7933  neips 7937  unnei 7945  lpval 7953  iscnp2 7971  cnpcl 7974  cnco 7978  cnpco 7979  iscncl 7980  cnsscnp 7982  cncnplem2 7985  cnconst 7990  metsym 8026  metge0 8029  metxplem3 8038  metxpdval 8039  metxptval 8040  metxpfval 8041  metxp 8044  bl2in 8053  blex 8059  blss 8063  blssex 8064  ssblex 8066  opnm 8070  opnin 8079  neibl 8087  lpbl 8090  methausi 8092  metcnconst 8096  metcnplem 8097  metcnp 8098  metcnpi3 8103  metcnpi4 8104  metcni2 8106  metcnp3 8107  metcnss 8109  bl2ioo 8122  ioo2bl 8123  blssioo 8124  tgioolem 8125  lmfval 8136  lmconst 8145  lmnn 8146  iscau3 8149  iscau4 8151  lmuni 8162  lmle 8171  metelcls 8176  metcld 8178  metcnp4 8181  xplmi 8184  xplm 8186  xpcn 8187  bopcnlem2 8193  fsumcnlem 8200  iscms2lem3 8202  lmcau 8207  cmsss 8208  cncms 8209  bcthlem1 8210  bcthlem2 8211  bcthlem7 8216  bcthlem8 8217  bcthlem13 8222  bcthlem14 8223  bcthlem18 8227  bcthlem19 8228  bcthlem20 8229  bcthlem21 8230  bcthlem24 8233  bcthlem25 8234  bcthlem26 8235  bcthlem30 8239  isgrpi 8255  grpidinvlem3 8263  grpidinvlem4 8264  grpidinv 8265  grprlidrid 8270  grpidinv2 8277  grpinvval 8284  grpinv 8286  grpasscan2 8295  grpinvf 8297  grpinvop 8298  grpdivfval 8299  grppncan 8308  grpnpcan 8309  grppnpcan2 8310  gxneg 8322  gxneg2 8323  gxcom 8325  gxsuc 8328  gxid 8329  gxnn0add 8330  gxnn0mul 8333  gxmul 8334  gxmodid 8335  grplactf1o 8339  gxdi 8355  subgid 8362  subgabl 8365  ghgrpilem3 8376  vcm 8437  invfval 8508  nvmul0or 8519  nvpncan2 8523  nvnncan 8530  nvdif 8540  nvpi 8541  nvabs 8548  nvge0 8549  nvgt0 8550  nv1 8551  imsdf 8567  imsmetlem 8570  nvlmle 8580  vacnlem3 8584  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  ipval2lem2 8608  ipval2 8611  4ipval2 8612  ipval2lem5 8614  4ipval3 8616  ipnm 8618  ipcl 8619  ipcj 8621  ip1cnilem4 8630  ip1cnilem5 8631  ip1cnilem6 8632  sspg 8641  ssps 8643  sspmlem 8645  sspz 8648  sspn 8649  lno0 8671  lnomul 8675  nmosetn0 8682  nmoge0 8684  nmoub3i 8690  nmo0 8706  nmlno0lem 8708  nmlnogt0 8712  nmblolbii 8714  isblo3i 8716  blometi 8718  blocnilem 8719  blocni 8720  phpar 8739  ipasslem2 8747  ipasslem4 8749  ipasslem8 8753  ipasslem9 8754  ipdi 8759  ipassr 8762  ipsubdir 8764  ipsubdi 8765  ip2eqi 8773  bnsscmcl 8785  ubthlem3 8789  ubthlem7 8793  ubthlem8 8794  ubthlem9 8795  ubthlem10 8796  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  ubthlem14 8802  minveclem9 8813  minveclem16 8820  minveclem21 8825  minveclem25 8829  minveclem30 8834  minveclem31 8835  minveclem36 8840  minveclem38 8842  hlipgt0 8878  htthlem7 8888  htthlem9 8890  htthlem11 8892  spwval2 8915  spwpr4 8925  spwpr4OLD 8926  spwpr4aOLD 8927  spwpr4c 8928  sincolem 8932  sinperlem1 8953  sinperlem2 8954  efimpi 8965  sineq0 8983  sineq0OLD 8984  sineq0re 8985  cosh111lem1 8986  efif 8993  efifolem5 8998  efifolem7 9000  efielcirc 9011  shftefif1olem 9013  eff1lem 9015  eff1i 9016  effoi 9017  resslogrn 9025  h2hcau 9124  hvsubdistr1 9191  hvsubdistr2 9192  hvmulcan 9214  hvmulcanOLD 9215  hvmulcan2 9216  hvsubcan2 9218  his2sub 9234  his6 9241  hi2eq 9247  normf 9265  normge0 9268  normgt0OLD 9269  normgt0 9270  norm-i 9272  hhph 9321  bcsiALT 9322  hcau2 9331  hhcms 9348  norm1 9397  norm1exi 9398  hhssnv 9410  hhsscms 9426  chocunii 9448  occllem6 9454  projlem2 9463  projlem25 9486  projlem26 9487  projlem28 9489  projlem30 9491  pjthlem7 9501  pjthlem10 9504  pjpo 9537  hsupval2 9576  spanssoc 9595  pjspansn 9776  spanunsni 9778  h1datomi 9780  fh1 9837  fh2 9838  cm2j 9839  osumlem6 9861  osumlem7 9862  nonbooli 9874  spansncvi 9875  5oalem1 9877  5oalem2 9878  3oalem2 9886  pjrni 9925  pjf 9931  pjnorm2 9950  mayete3i 9951  mayete3OLDi 9952  hosubcli 9975  hoaddcomi 9978  honegsubi 10002  homco1 10007  homulass 10008  hoadddi 10009  hoadddir 10010  adjsym 10039  eigposi 10042  cnvadj 10096  hhlnoi 10106  nmoplb 10111  nmopub2tALT 10113  nmopge0 10115  nmopgt0 10116  unoplin 10124  nmfnlb 10128  nmfnleub2 10130  nmfnge0 10131  adj2 10138  adjadj 10140  adjvalval 10141  hmoplin 10146  kbpj 10160  eighmre 10167  homco2 10180  hoddii 10193  nmlnop0iALT 10199  lnophsi 10205  lnopeqi 10212  nmopun 10218  nmbdoplbi 10228  nmcopexlem3 10232  nmcopexlem5 10234  nmcopexlem6 10235  nmcoplbi 10237  nmophmi 10240  lnopconi 10242  lnopcnbd 10244  nmbdfnlbi 10257  nmcfnexlem3 10261  nmcfnexlem5 10263  nmcfnexlem6 10264  nmcfnlbi 10266  lnfnconi 10269  lnfncnbd 10271  riesz3i 10274  cnlnadjlem2 10280  cnlnadjlem5 10283  cnlnadjlem6 10284  cnlnadjlem7 10285  adjbdln 10295  adjbd1o 10297  adjlnop 10298  nmopadjlem 10301  nmoptrii 10306  nmopcoi 10307  nmopcoadji 10313  branmfn 10317  branmfnOLD 10318  cnvbraval 10323  kbass2 10330  leop2 10337  leop3 10338  leoprf2 10340  leopmul 10347  leopmul2i 10348  leoptri 10349  leopnmid 10351  nmopleid 10352  pjnmopi 10355  hmopidmchlem 10358  hmopidmchi 10359  hmopidmpji 10360  pjsdii 10363  pjddii 10364  pjss2coi 10372  pjssposi 10380  pjhmopidm 10390  pjclem4 10408  pj3si 10416  pj3cor1i 10418  hstle1 10434  hstle 10438  sto2i 10445  staddi 10454  stadd3i 10456  strlem1 10458  strlem3a 10460  strlem5 10463  strlem6 10464  stri 10465  hstrlem6 10472  hstri 10473  jplem1 10476  golem1 10479  stcltrlem1 10484  dmdbr5 10516  mdslmd1lem1 10533  csmdsymi 10542  cvdmd 10545  atom1d 10561  superpos 10562  shatomici 10566  irredlem2 10600  atcvat3i 10605  atcvat4i 10606  mdsymlem1 10612  mdsymlem2 10613  mdsymlem6 10617  cdj1i 10642  cdj3lem2 10644  cdj3i 10650  ghomgrpilem2 10671  ghomfo 10676  ghomid 10679  ghomf1olem 10681  cayleylem2 10695  nnssi3 10705  nndivlub 10707  scprefat2 10784  njtlc 10804  fiv 10849  toplat 10884  idrval 10904  cmpidelt 10906  rnplrnml 10948  zerab 10957  zerab2 10958  multinv 10959  multinvb 10960  mult2inv 10961  isdivrng 10968  cdrci 10994  truni1 10999  truni3 11001  oibbi1 11004  oibbi2 11005  homeofval 11022  hmeogrp 11044  homindlem3 11053  stoig 11064  qusp 11068  fipfil 11076  fipfil2 11077  fgsb 11082  efilcp 11083  fgsb2 11086  efilcp2 11087  cnfilca 11088  sfvlim 11100  limfillem2 11102  altretop 11144  dmse1 11146  msr3 11148  mslb1 11152  2wsms 11153  msra3 11154  iintlem1 11155  trran 11159  trnij 11160  cnvtr 11161  rcmob 11203  imonclem 11268  icmpmon 11271  idsubfun 11312  xpss1 11403  xpss2 11404  finminlem 11418  fiuni 11420  elfiun 11421  fictblem 11422  fictb 11423  finsschain 11425  ordiso 11426  ordtypelem3 11429  ordtypelem5 11431  ordtypelem7 11433  hartog 11436  onsdom 11437  omsubsuc2 11439  omsublim 11448  infenomsub 11450  omsubinit 11451  opncldf1 11454  opncldf2 11455  opncldf3 11456  cldbnd 11462  clsun 11465  opnnei 11469  cnpnei 11472  cncls 11473  cnntr 11474  elsubsp 11477  subspid 11478  subsubtop 11479  subcld 11480  subcls 11481  subntr 11482  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem2 11497  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  connsub 11502  subtopmet 11506  reconnlem1 11507  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  reconn 11512  iccconn 11514  ivthALT 11515  2ndcsb 11537  2ndc1stc 11538  2ndcctbss 11539  fneint 11547  fness 11552  ssref 11553  fnetr 11556  reftr 11558  fnessref 11564  refssfne 11565  finlocfin 11570  locfincomp 11575  locfindsc 11576  locfincf 11577  comppfsc 11578  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  ist1-2 11603  ist1-3 11604  isnrm2 11613  fbssint 11626  filfbas 11628  opnfbas 11629  extbas1 11641  filrn 11643  isufil2 11650  ufileulem 11657  ufileu 11658  filufint 11659  uffixfr 11660  ufinffr 11663  ufilen 11664  limfilcf 11683  flimcls 11684  cnpfillim 11686  isfilmap 11689  elfilmap 11690  elfilmap2 11691  elfilmap3 11692  fmf 11693  fmbas 11694  filmapss 11696  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem3 11702  fmfnfmlem4 11703  fmfnfm 11704  filfm 11706  sflimf 11708  flimfbas 11713  sfcls 11716  isfclus 11718  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnplem 11729  fcluscomplem 11732  fcluscomp 11733  ufcomp 11734  isfclusf 11737  tailf 11756  istail 11757  tailuni 11761  tailfb 11762  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gaid 11776  ssga 11777  gapm 11784  sylancl 11785  raleqfn 11790  oprabco 11811  oprab2co 11812  oprabexd 11813  upxp 11822  upixp 11823  abrexdom 11826  fimax 11837  indexd 11846  indexf 11847  fipreima 11848  welb 11851  uzm1 11862  fzm1 11867  rddif 11869  absrdbnd 11870  mod0 11871  sdclem1 11875  sdc 11877  incsequz 11879  incsequz2 11880  nnubfi 11881  nninfnub 11882  fsum00 11883  fsumlt 11884  fsumlt1 11894  csbrni 11895  trirni 11896  subspopn 11900  subspcld 11901  subspabs 11903  metsstop 11909  blhalf 11911  mettrifi 11912  mettrifi2 11913  geomcau 11914  lmclim2 11915  metdcn 11918  iccsplit 11919  icoopnst 11940  iocopnst 11941  lincmb01cmp 11942  lincmb01icc 11943  cnimass 11949  cnres 11950  cnresima 11952  hmeocld 11961  tlmval 11964  tlmconst 11968  txbas 11973  tx1cn 11976  uptx 11978  txcnopab 11980  txsubsp 11983  sstotbnd 11992  totbndss 11993  isbnd3 11997  blbnd 11999  totbndbnd 12000  ismtyhmeolem 12006  ismtybndlem 12008  ismtyres 12010  heiborlem11 12021  heiborlem16 12026  heiborlem23 12033  heiborlem26 12036  heiborlem28 12038  heiborlem31 12041  heiborlem32 12042  heiborlem33 12043  heiborlem35 12045  heiborlem36 12046  heiborlem39 12049  bfplem3 12056  bfplem5 12058  recms 12066  rrnmet 12072  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  rrnheibor 12079  ismrer1 12080  reheibor 12081  iccbnd 12082  icccmp 12083  phtpyid 12091  phtpycom 12092  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain