Theorem syl22anc 852

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl22anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)

Assertion

Ref	Expression
syl22anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl22anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 521	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl22anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)
7	3, 4, 5, 6	syl12anc 850	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  preqsnd  4819  fr2nr  5635  soltmin  6148  f1oprg  6902  f1prex  7323  fveqf1o  7341  weniso  7395  fr3nr  7818  fnwe2lem3  8184  suppofssd  8258  smogt  8413  smocdmdom  8414  oacomf1o  8611  en2prd  9113  difsnen  9116  enfixsn  9143  domss2  9193  ssenen  9208  marypha1lem  9462  fisupcl  9499  ordtypelem3  9551  ordtypelem8  9556  oieu  9570  oismo  9571  wofib  9576  wemaplem2  9578  wemapso  9582  wemapso2lem  9583  unxpwdom2  9619  infdifsn  9695  oemapvali  9722  cantnflem1c  9725  cantnflem1  9727  cantnf  9731  cnfcom3  9742  r1ordg  9822  r1filimi  9940  dif1card  10128  infxpenlem  10131  dfac8clem  10150  infxp  10331  infmap2  10334  cflim2  10380  coftr  10390  fin2i2  10435  enfin2i  10438  fin23lem26  10442  fin23lem27  10445  fin23lem40  10468  isf32lem2  10471  isf32lem3  10472  isf32lem4  10473  isf32lem7  10476  isf32lem9  10478  fin1a2lem13  10529  fin12  10530  alephexp1  10703  gchdomtri  10753  fpwwe2lem11  10765  fpwwe2lem12  10766  gchpwdom  10794  gchhar  10803  adderpqlem  11078  mulerpqlem  11079  addassnq  11082  mulassnq  11083  distrnq  11085  mulidnq  11087  recmulnq  11088  ltexnq  11099  distrlem1pr  11149  distrlem4pr  11150  prlem936  11171  reclem3pr  11173  mulcmpblnr  11195  mulgt0d  11504  mul4d  11561  add4d  11578  add42d  11579  subcan  11652  addsub4d  11755  subadd4d  11756  sub4d  11757  2addsubd  11758  addsubeq4d  11759  muladdd  11813  mulsubd  11814  addgegt0d  11929  addgtge0d  11930  addge0d  11932  mulge0d  11933  le2subd  11976  ltleaddd  11977  leltaddd  11978  lt2subd  11980  divdivdiv  12058  divcan5  12059  divne0d  12149  recdivd  12150  recdiv2d  12151  divcan6d  12152  ddcand  12153  rec11d  12154  divmuldivd  12174  divmul13d  12175  divmul24d  12176  divadddivd  12177  divsubdivd  12178  divmuleqd  12179  divdivdivd  12180  mulge0b  12227  recreclt  12256  divgt0d  12292  mulgt1d  12293  lemulge11d  12294  lemulge12d  12295  ltmul12ad  12298  lemul12ad  12299  lemul12bd  12300  supmul1  12326  nndivtr  12425  qreccl  13137  ledivdivd  13229  lediv12ad  13263  lt2mul2divd  13273  xlt2add  13430  supxrun  13486  supxrre  13497  infxrre  13507  elicore  13569  iccss2  13588  iccssico2  13591  icossico2d  13592  lincmb01cmp  13666  iccf1o  13667  nnge2recico01  13678  fzrev2i  13763  2tnp1ge0ge0  14009  m1modnnsub1  14100  modaddmodup  14117  modaddmodlo  14118  modsubdir  14123  fzennn  14151  sermono  14217  mulexpz  14285  expaddz  14289  sqdiv  14304  expsubd  14340  ltexp2a  14349  expmordi  14350  leexp2a  14355  expmulnbnd  14420  digit1  14422  lt2sqd  14441  le2sqd  14442  sq11d  14443  bcm1k  14500  bcp1n  14501  bcp1nk  14502  hashpss  14595  hashf1lem1  14641  cshw1  15015  2swrd2eqwrdeq  15149  ofccat  15165  sgnmul  15303  absrele  15518  sqreulem  15571  sqrtmuld  15636  sqrtsq2d  15637  sqrtled  15638  sqrtltd  15639  sqr11d  15640  abs3lemd  15675  rlimuni  15761  climuni  15763  lo1resb  15775  o1resb  15777  2clim  15783  addcn2  15805  mulcn2  15807  o1of2  15824  o1rlimmul  15830  lo1add  15838  lo1mul  15839  isercolllem1  15876  caucvgrlem  15884  iseraltlem2  15894  iseraltlem3  15895  mptfzshft  15988  fsumrev  15989  fsum0diag2  15993  binomlem  16042  climcndslem1  16062  climcndslem2  16063  harmonic  16072  mertenslem1  16097  fprodser  16160  fprodrev  16188  efcllem  16287  moddvds  16477  dvds1  16533  dvdsext  16535  evennn2n  16565  bitsinv1  16656  sadaddlem  16680  sadasslem  16684  sadeq  16686  mulgcd  16765  lcmftp  16855  rpmulgcd2  16875  coprmproddvdslem  16881  isprm5  16927  isprm6  16934  crth  16999  eulerthlem2  17003  prmdiveq  17007  pythagtriplem11  17047  pythagtriplem13  17049  pcgcd1  17099  pcprmpw2  17104  pcaddlem  17110  fldivp1  17119  4sqlem12  17178  4sqlem14  17180  4sqlem15  17181  4sqlem16  17182  vdwapun  17196  mreexexlem4d  17871  acsfn1  17885  acsfn2  17887  sscpwex  18040  rescabs  18058  yonedainv  18505  chnub  18846  subm0  19061  pmtrfb  19730  psgnunilem1  19758  odmodnn0  19805  odeq  19815  dfod2  19829  sylow1lem1  19863  lsmsubg  19919  lsmmod  19940  lsmdisj2  19947  ghmplusg  20111  odadd  20115  gexexlem  20117  lt6abl  20160  cyggex2  20162  dprdfinv  20286  dmdprdsplitlem  20304  dpjidcl  20325  ablfacrp  20333  ablfacrp2  20334  ablfac1c  20338  ablfac1eu  20340  omndadd2d  20395  omndadd2rd  20396  omndmul2  20398  acsfn1p  21107  lcomfsupp  21228  lssvancl1  21271  lssvnegcl  21282  lspprvacl  21325  ellspsni  21327  lspsn  21328  lmhmplusg  21370  lmhmima  21373  lmhmpreima  21374  reslmhm  21378  lbsind2  21407  lsmcl  21409  lsmelval2  21411  lsppreli  21416  lspprabs  21421  pj1lmhm  21426  lssvs0or  21439  lspabs3  21450  lspfixed  21457  lspexch  21458  lsmcv  21470  lspsolv  21472  lidlmcld  21557  drngnidl  21582  rhmpreimaidl  21622  rngqiprngimfo  21648  rngqiprngfulem4  21661  isprmidlc  21679  rhmpreimaprmidl  21686  qsidomlem1  21687  ssdifidllem  21691  gzrngunit  21793  zringlpirlem3  21825  prmirredlem  21833  znf1o  21912  znunithash  21925  freshmansdream  21935  ofldchr  21937  frlmsubgval  22126  frlmvplusgvalc  22128  frlmvscaval  22129  frlmphllem  22141  frlmphl  22142  frlmssuvc1  22155  frlmsslsp  22157  frlmup1  22159  frlmup2  22160  lindfind2  22179  lindfrn  22182  f1lindf  22183  islindf4  22199  mplbas2  22406  evlslem3  22444  evlslem1  22446  evladdval  22467  evlmulval  22468  evlsaddval  22493  evlsmulval  22494  coe1addfv  22639  lply1binom  22683  evl1addd  22714  evl1subd  22715  evl1muld  22716  mamudi  22773  mamudir  22774  1marepvmarrepid  22945  mdetrlin  22972  smadiadetglem1  23041  smadiadetg  23043  cramerimplem1  23056  mat2pmatscmxcl  23113  m2pmfzgsumcl  23121  pmatcollpw  23154  pmatcollpwfi  23155  pmatcollpw3fi1lem1  23159  cpmidpmatlem2  23244  cpmadugsumlemF  23249  chcoeffeqlem  23258  ntrin  23434  topssnei  23497  restbas  23531  restntr  23555  cnntri  23644  fiuncmp  23777  nllyrest  23860  nllyidm  23863  hausllycmp  23868  cldllycmp  23869  hauspwdom  23875  txcld  23977  txcn  24000  txlly  24010  txnlly  24011  txhaus  24021  txlm  24022  txkgen  24026  xkococnlem  24033  cnmpt2res  24051  xkoinjcn  24061  basqtop  24085  qtopeu  24090  trfbas2  24217  neifil  24254  hausflim  24355  alexsubALTlem2  24422  cnextfval  24436  cnextfvval  24439  cnextf  24440  cnextfres  24443  clssubg  24483  utop2nei  24624  utop3cls  24625  utopreg  24626  psmetlecl  24689  xmetlecl  24720  prdsxmetlem  24742  bldisj  24772  imasf1obl  24862  prdsbl  24865  stdbdmet  24890  stdbdmopn  24892  met2ndci  24896  metcnp  24915  metustto  24927  metustexhalf  24930  cfilucfil  24933  metucn  24945  lssnlm  25075  nmotri  25113  nmoid  25116  tgioo  25170  blcvx  25172  xrsmopn  25187  reperflem  25193  reconnlem2  25202  opnreen  25206  metdsge  25224  metdsre  25228  metdscnlem  25230  metnrmlem1a  25233  metnrmlem1  25234  metnrmlem3  25236  cncfmet  25285  cnmpopc  25304  icopnfcnv  25318  icopnfhmeo  25319  cnllycmp  25332  evth  25335  lebnumii  25342  nmoleub2lem3  25491  iscfil2  25642  cfil3i  25645  iscfil3  25649  cfilfcls  25650  iscau3  25654  iscmet3lem2  25668  caubl  25684  lmcau  25689  cssbn  25751  rrxcph  25768  minveclem2  25802  pjthlem1  25813  pjthlem2  25814  ivthicc  25834  ovollecl  25859  ovolunlem1a  25872  ovolunnul  25876  ovoliunlem1  25878  ismbl2  25903  nulmbl2  25912  unmbl  25913  volun  25921  voliunlem2  25927  ioombl1lem2  25935  uniioombllem2a  25958  uniioombllem3  25961  uniioombllem4  25962  dyaddisjlem  25971  dyadmaxlem  25973  opnmbllem  25977  volsup2  25981  volcn  25982  ismbfd  26015  mbfi1fseqlem1  26091  mbfi1fseqlem5  26095  itg2lecl  26114  itg2monolem2  26127  itg2gt0  26136  itgspliticc  26212  ellimc3  26254  limcres  26261  dvfval  26272  dvres3  26288  dvres3a  26289  dvmptresicc  26291  dvnff  26298  dvnadd  26304  dvn2bss  26305  dvnres  26306  dvcmul  26319  dvcmulf  26320  dvmptres3  26331  dvmptres2  26337  dvmptntr  26346  dvexp3  26353  dvferm1lem  26359  dvlip  26368  dvlipcn  26369  dvlip2  26370  c1liplem1  26371  dvgt0lem1  26377  dvgt0lem2  26378  dvne0  26386  lhop1lem  26388  lhop2  26390  lhop  26391  dvcnvrelem1  26392  dvcnvrelem2  26393  dvcvx  26395  dvfsumle  26396  dvfsumabs  26398  dvfsumlem2  26402  ftc1lem6  26416  ftc1  26417  ftc2ditglem  26420  itgsubstlem  26423  itgpowd  26425  tdeglem4  26433  mdegaddle  26447  mdegmullem  26451  ply1rem  26539  fta1glem2  26542  fta1blem  26544  ig1peu  26548  ig1pdvds  26553  dgrmulc  26645  dgrcolem1  26647  plydivlem4  26672  plydiveu  26674  fta1lem  26683  vieta1lem1  26688  vieta1lem2  26689  plyexmo  26691  rngunsnply  26693  taylfvallem1  26741  taylfval  26743  tayl0  26746  taylplem1  26747  taylply2  26752  taylply  26753  dvtaylp  26754  dvntaylp  26755  dvntaylp0  26756  taylthlem1  26757  taylthlem2  26758  ulmcaulem  26778  ulmcau  26779  ulmcn  26783  ulmdvlem1  26784  radcnvlem1  26797  radcnvle  26804  psercn  26810  pserdvlem2  26812  pserdv  26813  abelth  26825  tanregt0  26924  dvlog2lem  27037  efopn  27043  logtayllem  27044  logccv  27048  cxplt3  27085  cxpmul2zd  27101  cxpltd  27104  cxpled  27105  cxplt3d  27120  cxple3d  27121  dvsqrt  27127  cxpcn3  27133  cxpaddle  27137  cxpeq  27142  angcan  27187  angvald  27189  ang180lem2  27195  ang180  27199  isosctrlem3  27205  dquartlem1  27236  atantayl2  27323  leibpi  27327  log2tlbnd  27330  birthdaylem3  27338  xrlimcnp  27353  efrlim  27354  o1cxp  27359  jensenlem2  27372  jensen  27373  fsumharmonic  27396  lgamucov  27422  lgamcvg2  27439  wilthlem1  27452  basellem3  27467  basellem6  27470  basellem8  27472  ppisval  27488  chtwordi  27540  ppiwordi  27546  mumullem2  27564  mpodvdsmulf1o  27578  dvdsmulf1o  27580  fsumvma  27597  fsumvma2  27598  chpchtsum  27603  chpub  27604  logfacubnd  27605  dchrmulcl  27633  dchrinv  27645  dchrptlem1  27648  dchrptlem2  27649  sumdchr2  27654  dchr2sum  27657  bposlem7  27674  lgslem1  27681  lgslem3  27683  lgsdirprm  27715  lgsqrlem2  27731  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem4  27762  lgseisen  27763  lgsquadlem1  27764  lgsquad2lem1  27768  lgsquad3  27771  m1lgs  27772  2sqlem7  27808  2sq2  27817  2sqmod  27820  chebbnd1lem2  27854  chebbnd1lem3  27855  rplogsumlem1  27868  rpvmasumlem  27871  dchrvmasumlem1  27879  dchrvmasum2lem  27880  dchrvmasumlema  27884  dchrisum0flblem2  27893  dchrisum0fno1  27895  dchrisum0re  27897  logdivsum  27917  pntrsumbnd2  27951  pntpbnd1a  27969  pntpbnd1  27970  pntibndlem2  27975  pntlemr  27986  pntlemj  27987  pntlemf  27989  pnt2  27997  padicabv  28014  ostth2lem2  28018  lesrecd  28243  ltsrecd  28245  madebday  28343  addsproplem6  28417  negsproplem6  28476  mulsproplem13  28571  mulsproplem14  28572  ltmulsd  28580  mulsgt0d  28588  angmgmaddov2  29446  f1otrg  29505  brbtwn2  29540  colinearalglem2  29542  axcgrtr  29550  axcgrid  29551  axsegconlem7  29558  axsegcon  29562  ax5seglem3  29566  ax5seglem6  29569  ax5seg  29573  axpaschlem  29575  axlowdimlem17  29593  axcontlem2  29600  axcontlem4  29602  axcontlem7  29605  axcontlem8  29606  ecgrtg  29618  usgredg2v  29865  vtxdgoddnumeven  30191  2trlond  30585  eupthp1  30874  nmobndi  31434  ubthlem2  31530  ubthlem3  31531  minvecolem2  31534  shuni  31959  pjhthlem1  32050  chscllem2  32297  pjcompi  32331  mayete3i  32387  unoplin  32579  hmoplin  32601  nmophmi  32690  mdslmd4i  32992  isoun  33392  submuladdd  33428  receqid  33432  xrge0addcld  33450  xrofsup  33455  eliccelico  33465  elicoelioo  33466  difioo  33470  rexdiv  33588  mgcmnt1d  33657  mgcmnt2d  33658  xrge0addgt0  33677  cycpmcl  33776  cycpm2tr  33779  cyc3evpm  33810  cycpmconjslem2  33815  edompidlem  33960  fldgensdrg  33980  qusker  34014  eqgvscpbl  34015  ringlsmss1  34053  ringlsmss2  34054  intlidl  34074  lidlunitel  34077  elrspunidl  34082  idlinsubrg  34085  mxidlmaxv  34097  mxidlprm  34099  ssmxidllem  34102  opprmxidlabs  34115  qsdrnglem2  34124  dflring3  34133  dflring4  34134  selvply1rhmlem4  34266  mplvrpmmhm  34289  mplvrpmrhm  34290  esplyind  34318  resssra  34330  ply1degltdimlem  34365  lindsunlem  34367  sdrgfldext  34393  fldsdrgfldext  34404  finexttrb  34408  fldgenfldext  34411  fldextrspunlem1  34418  algextdeglem4  34463  algextdeglem8  34467  constrextdg2lem  34491  mdetpmtr2  34567  mdetpmtr12  34568  madjusmdetlem1  34570  madjusmdetlem4  34573  rhmpreimacn  34628  unitdivcld  34644  xrge0mulc1cn  34684  qqhnm  34733  esumcst  34806  esumfsup  34813  esumpmono  34822  esumcvg  34829  sigapisys  34899  sigapildsys  34906  ldgenpisyslem1  34907  1stmbfm  35003  2ndmbfm  35004  dya2icoseg  35020  omssubadd  35043  sibfinima  35082  probmeasb  35173  orvcgteel  35211  orvclteel  35216  ballotlemsima  35259  ballotlemfrceq  35272  ccatmulgnn0dir  35285  fct2relem  35337  ftc2re  35338  chtvalz  35369  subfacp1lem2a  36153  subfaclim  36161  erdsze2lem2  36177  cvmliftlem2  36259  cvmliftlem10  36267  cvmliftlem13  36269  cvmliftiota  36274  cvmlift2lem9  36284  cvmlift2lem11  36286  cvmlift2lem12  36287  cvmliftphtlem  36290  cvmlift3lem6  36297  cvmlift3lem7  36298  cvmlift3lem9  36300  snmlff  36302  mrsubfval  36481  wzel  36801  wsuclem  36802  brsegle  37088  nmulel1  37179  nadddilem1  37184  nadddilem3  37186  opnregcld  37333  weiunfrlem  37467  fin2so  38798  poimirlem17  38823  poimirlem23  38829  opnmbllem0  38842  mblfinlem3  38845  mblfinlem4  38846  itg2addnclem  38857  itg2addnc  38860  itg2gt0cn  38861  ftc1cnnclem  38877  ftc1cnnc  38878  areacirclem5  38898  indexdom  38936  sstotbnd2  38974  isbnd3  38984  isbnd3b  38985  cntotbnd  38996  ismtyima  39003  heibor1lem  39009  heiborlem8  39018  rrncmslem  39032  reheibor  39039  lkrlsp  40425  lshpkrlem5  40437  ldualssvscl  40481  ldualssvsubcl  40482  llnmlplnN  40862  llncvrlpln  40881  pmapjat1  41176  pclfinN  41223  lautlt  41414  lauteq  41418  lautco  41420  ltrn11  41449  ltrnle  41452  ltrneq2  41471  cdlemednuN  41623  cdleme20k  41642  cdleme20l2  41644  cdleme20l  41645  cdleme20m  41646  cdleme21c  41650  cdleme22e  41667  cdleme22eALTN  41668  cdlemefrs32fva  41723  cdlemg4g  41939  cdlemg18b  42002  cdlemg18c  42003  cdlemj3  42146  dia2dimlem5  42391  dvhopN  42439  cdlemm10N  42441  dihjatcclem4  42744  dochexmidlem2  42784  lclkrlem2o  42844  lcfrlem5  42869  lcfrlem6  42870  lcdlssvscl  42929  mapdpglem6  43001  mapdpglem9  43003  mapdpglem12  43006  mapdpglem14  43008  mapdindp0  43042  hdmaprnlem7N  43178  hdmaprnlem8N  43179  hdmaprnlem3eN  43181  hgmapvvlem3  43248  dvun  43676  addinvcom  43749  mzpsubst  44025  eldioph2lem1  44037  eldioph2lem2  44038  eldioph2b  44040  diophin  44049  irrapxlem2  44096  irrapxlem4  44098  irrapxlem5  44099  pellexlem1  44102  pellexlem2  44103  pellexlem6  44107  elpell1qr2  44145  pell1qrgaplem  44146  pell1qrgap  44147  pellqrex  44152  pellfundex  44159  pellfund14  44171  rmspecsqrtnq  44179  rmxyadd  44194  congsub  44243  mzpcong  44245  congrep  44246  acongtr  44251  acongrep  44253  jm2.19lem1  44262  jm2.22  44268  jm2.23  44269  jm2.26lem3  44274  jm2.26  44275  jm2.27a  44278  aomclem6  44327  hbtlem2  44391  hbtlem4  44393  hbtlem5  44395  dgraa0p  44416  proot1hash  44458  nnoeomeqom  44575  cantnf2  44588  omabs2  44595  naddcnff  44625  naddcnffo  44627  naddcnfcom  44629  naddcnfid1  44630  expgrowth  45580  fpmd  46548  abslt2sqd  46645  ioondisj2  46778  ioondisj1  46779  eliocre  46794  ioossioobi  46802  iooiinicc  46827  iooiinioc  46841  lptioo2  46916  limcresiooub  46925  limsupequzlem  47005  xlimmnfvlem2  47116  xlimpnfvlem2  47120  cncfuni  47169  cncfiooicclem1  47176  cxpcncf2  47182  dvcnre  47199  dvresntr  47201  dvresioo  47204  dvbdfbdioolem1  47211  dvnmptdivc  47221  dvnxpaek  47225  itgsinexplem1  47237  itgcoscmulx  47252  itgiccshift  47263  itgperiod  47264  ovolsplit  47271  stoweidlem11  47294  stoweidlem26  47309  stoweidlem34  47317  stoweidlem36  47319  stoweidlem38  47321  stirlinglem5  47361  dirkercncflem2  47387  dirkercncflem4  47389  fourierdlem20  47410  fourierdlem58  47447  fourierdlem72  47461  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem79  47468  fourierdlem80  47469  fourierdlem87  47476  fourierdlem94  47483  fourierdlem103  47492  fourierdlem104  47493  fourierdlem107  47496  fourierdlem113  47502  sqwvfoura  47511  sqwvfourb  47512  fourierswlem  47513  fouriersw  47514  etransclem46  47563  etransclem47  47564  rrndistlt  47573  rrnprjdstle  47584  ioorrnopnxrlem  47589  sge0ssre  47680  sge0seq  47729  hsphoidmvle2  47868  hsphoidmvle  47869  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmvlelem1  47878  hoidifhspdmvle  47903  hoiqssbllem2  47906  ovolval5lem2  47936  iinhoiicc  47957  iunhoiioo  47959  vonioolem2  47964  vonicclem2  47967  issmflem  48010  sqrtnnaa  48186  submodlt  48699  iccpartdisj  48792  m1expevenALTV  49018  fpprel2  49112  tgoldbach  49188  opstrgric  49297  gpg3kgrtriex  49460  nn0eo  49971  fdivpm  49986  refdivpm  49987  elbigolo1  50000  logbpw2m1  50010  fllog2  50011  dignn0flhalflem1  50058  dignn0flhalflem2  50059  itsclinecirc0in  50218  2itscplem2  50222  itscnhlinecirc02plem1  50225  iccdisj2  50342  tanhaddd  51259