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  4813  fr2nr  5628  soltmin  6132  f1oprg  6876  f1prex  7296  fveqf1o  7314  weniso  7368  fr3nr  7790  fnwe2lem3  8154  suppofssd  8228  smogt  8383  smocdmdom  8384  oacomf1o  8581  en2prd  9083  difsnen  9086  enfixsn  9113  domss2  9163  ssenen  9178  marypha1lem  9432  fisupcl  9469  ordtypelem3  9521  ordtypelem8  9526  oieu  9540  oismo  9541  wofib  9546  wemaplem2  9548  wemapso  9552  wemapso2lem  9553  unxpwdom2  9589  infdifsn  9665  oemapvali  9692  cantnflem1c  9695  cantnflem1  9697  cantnf  9701  cnfcom3  9712  r1ordg  9792  r1filimi  9910  dif1card  10096  infxpenlem  10099  dfac8clem  10118  infxp  10299  infmap2  10302  cflim2  10348  coftr  10358  fin2i2  10403  enfin2i  10406  fin23lem26  10410  fin23lem27  10413  fin23lem40  10436  isf32lem2  10439  isf32lem3  10440  isf32lem4  10441  isf32lem7  10444  isf32lem9  10446  fin1a2lem13  10497  fin12  10498  alephexp1  10671  gchdomtri  10721  fpwwe2lem11  10733  fpwwe2lem12  10734  gchpwdom  10762  gchhar  10771  adderpqlem  11046  mulerpqlem  11047  addassnq  11050  mulassnq  11051  distrnq  11053  mulidnq  11055  recmulnq  11056  ltexnq  11067  distrlem1pr  11117  distrlem4pr  11118  prlem936  11139  reclem3pr  11141  mulcmpblnr  11163  mulgt0d  11472  mul4d  11529  add4d  11546  add42d  11547  subcan  11620  addsub4d  11723  subadd4d  11724  sub4d  11725  2addsubd  11726  addsubeq4d  11727  muladdd  11781  mulsubd  11782  addgegt0d  11896  addgtge0d  11897  addge0d  11899  mulge0d  11900  le2subd  11943  ltleaddd  11944  leltaddd  11945  lt2subd  11947  divdivdiv  12025  divcan5  12026  divne0d  12116  recdivd  12117  recdiv2d  12118  divcan6d  12119  ddcand  12120  rec11d  12121  divmuldivd  12141  divmul13d  12142  divmul24d  12143  divadddivd  12144  divsubdivd  12145  divmuleqd  12146  divdivdivd  12147  mulge0b  12194  recreclt  12223  divgt0d  12259  mulgt1d  12260  lemulge11d  12261  lemulge12d  12262  ltmul12ad  12265  lemul12ad  12266  lemul12bd  12267  supmul1  12293  nndivtr  12392  qreccl  13104  ledivdivd  13196  lediv12ad  13230  lt2mul2divd  13240  xlt2add  13397  supxrun  13453  supxrre  13464  infxrre  13474  elicore  13536  iccss2  13555  iccssico2  13558  icossico2d  13559  lincmb01cmp  13633  iccf1o  13634  nnge2recico01  13645  fzrev2i  13730  2tnp1ge0ge0  13976  m1modnnsub1  14067  modaddmodup  14084  modaddmodlo  14085  modsubdir  14090  fzennn  14118  sermono  14184  mulexpz  14252  expaddz  14256  sqdiv  14271  expsubd  14307  ltexp2a  14316  expmordi  14317  leexp2a  14322  expmulnbnd  14386  digit1  14388  lt2sqd  14407  le2sqd  14408  sq11d  14409  bcm1k  14466  bcp1n  14467  bcp1nk  14468  hashpss  14561  hashf1lem1  14607  cshw1  14981  2swrd2eqwrdeq  15115  ofccat  15131  sgnmul  15269  absrele  15484  sqreulem  15536  sqrtmuld  15601  sqrtsq2d  15602  sqrtled  15603  sqrtltd  15604  sqr11d  15605  abs3lemd  15640  rlimuni  15726  climuni  15728  lo1resb  15740  o1resb  15742  2clim  15748  addcn2  15770  mulcn2  15772  o1of2  15789  o1rlimmul  15795  lo1add  15803  lo1mul  15804  isercolllem1  15841  caucvgrlem  15849  iseraltlem2  15859  iseraltlem3  15860  mptfzshft  15953  fsumrev  15954  fsum0diag2  15958  binomlem  16007  climcndslem1  16027  climcndslem2  16028  harmonic  16037  mertenslem1  16062  fprodser  16125  fprodrev  16153  efcllem  16252  moddvds  16442  dvds1  16498  dvdsext  16500  evennn2n  16530  bitsinv1  16621  sadaddlem  16645  sadasslem  16649  sadeq  16651  mulgcd  16730  lcmftp  16820  rpmulgcd2  16840  coprmproddvdslem  16846  isprm5  16892  isprm6  16899  crth  16964  eulerthlem2  16968  prmdiveq  16972  pythagtriplem11  17012  pythagtriplem13  17014  pcgcd1  17064  pcprmpw2  17069  pcaddlem  17075  fldivp1  17084  4sqlem12  17143  4sqlem14  17145  4sqlem15  17146  4sqlem16  17147  vdwapun  17161  mreexexlem4d  17830  acsfn1  17844  acsfn2  17846  sscpwex  17999  rescabs  18017  yonedainv  18464  chnub  18805  subm0  19020  pmtrfb  19688  psgnunilem1  19716  odmodnn0  19763  odeq  19773  dfod2  19787  sylow1lem1  19821  lsmsubg  19877  lsmmod  19898  lsmdisj2  19905  ghmplusg  20069  odadd  20073  gexexlem  20075  lt6abl  20118  cyggex2  20120  dprdfinv  20244  dmdprdsplitlem  20262  dpjidcl  20283  ablfacrp  20291  ablfacrp2  20292  ablfac1c  20296  ablfac1eu  20298  omndadd2d  20353  omndadd2rd  20354  omndmul2  20356  acsfn1p  21065  lcomfsupp  21186  lssvancl1  21229  lssvnegcl  21240  lspprvacl  21283  ellspsni  21285  lspsn  21286  lmhmplusg  21328  lmhmima  21331  lmhmpreima  21332  reslmhm  21336  lbsind2  21365  lsmcl  21367  lsmelval2  21369  lsppreli  21374  lspprabs  21379  pj1lmhm  21384  lssvs0or  21397  lspabs3  21408  lspfixed  21415  lspexch  21416  lsmcv  21428  lspsolv  21430  lidlmcld  21515  drngnidl  21540  rhmpreimaidl  21580  rngqiprngimfo  21606  rngqiprngfulem4  21619  isprmidlc  21637  rhmpreimaprmidl  21644  qsidomlem1  21645  ssdifidllem  21649  gzrngunit  21748  zringlpirlem3  21779  prmirredlem  21787  znf1o  21866  znunithash  21879  freshmansdream  21889  ofldchr  21891  frlmsubgval  22080  frlmvplusgvalc  22082  frlmvscaval  22083  frlmphllem  22095  frlmphl  22096  frlmssuvc1  22109  frlmsslsp  22111  frlmup1  22113  frlmup2  22114  lindfind2  22133  lindfrn  22136  f1lindf  22137  islindf4  22153  mplbas2  22360  evlslem3  22398  evlslem1  22400  evladdval  22421  evlmulval  22422  evlsaddval  22447  evlsmulval  22448  coe1addfv  22593  lply1binom  22637  evl1addd  22668  evl1subd  22669  evl1muld  22670  mamudi  22727  mamudir  22728  1marepvmarrepid  22899  mdetrlin  22926  smadiadetglem1  22995  smadiadetg  22997  cramerimplem1  23010  mat2pmatscmxcl  23067  m2pmfzgsumcl  23075  pmatcollpw  23108  pmatcollpwfi  23109  pmatcollpw3fi1lem1  23113  cpmidpmatlem2  23198  cpmadugsumlemF  23203  chcoeffeqlem  23212  ntrin  23388  topssnei  23451  restbas  23485  restntr  23509  cnntri  23598  fiuncmp  23731  nllyrest  23814  nllyidm  23817  hausllycmp  23822  cldllycmp  23823  hauspwdom  23829  txcld  23931  txcn  23954  txlly  23964  txnlly  23965  txhaus  23975  txlm  23976  txkgen  23980  xkococnlem  23987  cnmpt2res  24005  xkoinjcn  24015  basqtop  24039  qtopeu  24044  trfbas2  24171  neifil  24208  hausflim  24309  alexsubALTlem2  24376  cnextfval  24390  cnextfvval  24393  cnextf  24394  cnextfres  24397  clssubg  24437  utop2nei  24578  utop3cls  24579  utopreg  24580  psmetlecl  24643  xmetlecl  24674  prdsxmetlem  24696  bldisj  24726  imasf1obl  24816  prdsbl  24819  stdbdmet  24844  stdbdmopn  24846  met2ndci  24850  metcnp  24869  metustto  24881  metustexhalf  24884  cfilucfil  24887  metucn  24899  lssnlm  25029  nmotri  25067  nmoid  25070  tgioo  25124  blcvx  25126  xrsmopn  25141  reperflem  25147  reconnlem2  25156  opnreen  25160  metdsge  25178  metdsre  25182  metdscnlem  25184  metnrmlem1a  25187  metnrmlem1  25188  metnrmlem3  25190  cncfmet  25239  cnmpopc  25258  icopnfcnv  25272  icopnfhmeo  25273  cnllycmp  25286  evth  25289  lebnumii  25296  nmoleub2lem3  25445  iscfil2  25596  cfil3i  25599  iscfil3  25603  cfilfcls  25604  iscau3  25608  iscmet3lem2  25622  caubl  25638  lmcau  25643  cssbn  25705  rrxcph  25722  minveclem2  25756  pjthlem1  25767  pjthlem2  25768  ivthicc  25788  ovollecl  25813  ovolunlem1a  25826  ovolunnul  25830  ovoliunlem1  25832  ismbl2  25857  nulmbl2  25866  unmbl  25867  volun  25875  voliunlem2  25881  ioombl1lem2  25889  uniioombllem2a  25912  uniioombllem3  25915  uniioombllem4  25916  dyaddisjlem  25925  dyadmaxlem  25927  opnmbllem  25931  volsup2  25935  volcn  25936  ismbfd  25969  mbfi1fseqlem1  26045  mbfi1fseqlem5  26049  itg2lecl  26068  itg2monolem2  26081  itg2gt0  26090  itgspliticc  26166  ellimc3  26208  limcres  26215  dvfval  26226  dvres3  26242  dvres3a  26243  dvmptresicc  26245  dvnff  26252  dvnadd  26258  dvn2bss  26259  dvnres  26260  dvcmul  26273  dvcmulf  26274  dvmptres3  26285  dvmptres2  26291  dvmptntr  26300  dvexp3  26307  dvferm1lem  26313  dvlip  26322  dvlipcn  26323  dvlip2  26324  c1liplem1  26325  dvgt0lem1  26331  dvgt0lem2  26332  dvne0  26340  lhop1lem  26342  lhop2  26344  lhop  26345  dvcnvrelem1  26346  dvcnvrelem2  26347  dvcvx  26349  dvfsumle  26350  dvfsumabs  26352  dvfsumlem2  26356  ftc1lem6  26370  ftc1  26371  ftc2ditglem  26374  itgsubstlem  26377  itgpowd  26379  tdeglem4  26387  mdegaddle  26401  mdegmullem  26405  ply1rem  26493  fta1glem2  26496  fta1blem  26498  ig1peu  26502  ig1pdvds  26507  dgrmulc  26599  dgrcolem1  26601  plydivlem4  26626  plydiveu  26628  fta1lem  26637  vieta1lem1  26642  vieta1lem2  26643  plyexmo  26645  taylfvallem1  26693  taylfval  26695  tayl0  26698  taylplem1  26699  taylply2  26704  taylply  26705  dvtaylp  26706  dvntaylp  26707  dvntaylp0  26708  taylthlem1  26709  taylthlem2  26710  ulmcaulem  26730  ulmcau  26731  ulmcn  26735  ulmdvlem1  26736  radcnvlem1  26749  radcnvle  26756  psercn  26762  pserdvlem2  26764  pserdv  26765  abelth  26777  tanregt0  26876  dvlog2lem  26989  efopn  26995  logtayllem  26996  logccv  27000  cxplt3  27037  cxpmul2zd  27053  cxpltd  27056  cxpled  27057  cxplt3d  27072  cxple3d  27073  dvsqrt  27079  cxpcn3  27085  cxpaddle  27089  cxpeq  27094  angcan  27139  angvald  27141  ang180lem2  27147  ang180  27151  isosctrlem3  27157  dquartlem1  27188  atantayl2  27275  leibpi  27279  log2tlbnd  27282  birthdaylem3  27290  xrlimcnp  27305  efrlim  27306  o1cxp  27311  jensenlem2  27324  jensen  27325  fsumharmonic  27348  lgamucov  27374  lgamcvg2  27391  wilthlem1  27404  basellem3  27419  basellem6  27422  basellem8  27424  ppisval  27440  chtwordi  27492  ppiwordi  27498  mumullem2  27516  mpodvdsmulf1o  27530  dvdsmulf1o  27532  fsumvma  27549  fsumvma2  27550  chpchtsum  27555  chpub  27556  logfacubnd  27557  dchrmulcl  27585  dchrinv  27597  dchrptlem1  27600  dchrptlem2  27601  sumdchr2  27606  dchr2sum  27609  bposlem7  27626  lgslem1  27633  lgslem3  27635  lgsdirprm  27667  lgsqrlem2  27683  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem4  27714  lgseisen  27715  lgsquadlem1  27716  lgsquad2lem1  27720  lgsquad3  27723  m1lgs  27724  2sqlem7  27760  2sq2  27769  2sqmod  27772  chebbnd1lem2  27806  chebbnd1lem3  27807  rplogsumlem1  27820  rpvmasumlem  27823  dchrvmasumlem1  27831  dchrvmasum2lem  27832  dchrvmasumlema  27836  dchrisum0flblem2  27845  dchrisum0fno1  27847  dchrisum0re  27849  logdivsum  27869  pntrsumbnd2  27903  pntpbnd1a  27921  pntpbnd1  27922  pntibndlem2  27927  pntlemr  27938  pntlemj  27939  pntlemf  27941  pnt2  27949  padicabv  27966  ostth2lem2  27970  lesrecd  28195  ltsrecd  28197  madebday  28295  addsproplem6  28369  negsproplem6  28428  mulsproplem13  28523  mulsproplem14  28524  ltmulsd  28532  mulsgt0d  28540  angmgmaddov2  29398  f1otrg  29457  brbtwn2  29492  colinearalglem2  29494  axcgrtr  29502  axcgrid  29503  axsegconlem7  29510  axsegcon  29514  ax5seglem3  29518  ax5seglem6  29521  ax5seg  29525  axpaschlem  29527  axlowdimlem17  29545  axcontlem2  29552  axcontlem4  29554  axcontlem7  29557  axcontlem8  29558  ecgrtg  29570  usgredg2v  29817  vtxdgoddnumeven  30143  2trlond  30537  eupthp1  30826  nmobndi  31386  ubthlem2  31482  ubthlem3  31483  minvecolem2  31486  shuni  31911  pjhthlem1  32002  chscllem2  32249  pjcompi  32283  mayete3i  32339  unoplin  32531  hmoplin  32553  nmophmi  32642  mdslmd4i  32944  isoun  33346  submuladdd  33382  receqid  33386  xrge0addcld  33404  xrofsup  33409  eliccelico  33419  elicoelioo  33420  difioo  33424  rexdiv  33542  mgcmnt1d  33608  mgcmnt2d  33609  xrge0addgt0  33628  cycpmcl  33727  cycpm2tr  33730  cyc3evpm  33761  cycpmconjslem2  33766  fldgensdrg  33926  qusker  33960  eqgvscpbl  33961  ringlsmss1  33999  ringlsmss2  34000  intlidl  34020  lidlunitel  34023  elrspunidl  34028  idlinsubrg  34031  mxidlmaxv  34043  mxidlprm  34045  ssmxidllem  34048  opprmxidlabs  34061  qsdrnglem2  34070  dflring3  34079  dflring4  34080  selvply1rhmlem4  34205  mplvrpmmhm  34228  mplvrpmrhm  34229  esplyind  34257  resssra  34269  ply1degltdimlem  34304  lindsunlem  34306  sdrgfldext  34332  fldsdrgfldext  34343  finexttrb  34347  fldgenfldext  34350  fldextrspunlem1  34357  algextdeglem4  34402  algextdeglem8  34406  constrextdg2lem  34430  mdetpmtr2  34506  mdetpmtr12  34507  madjusmdetlem1  34509  madjusmdetlem4  34512  rhmpreimacn  34567  unitdivcld  34583  xrge0mulc1cn  34623  qqhnm  34672  esumcst  34745  esumfsup  34752  esumpmono  34761  esumcvg  34768  sigapisys  34838  sigapildsys  34845  ldgenpisyslem1  34846  1stmbfm  34942  2ndmbfm  34943  dya2icoseg  34959  omssubadd  34982  sibfinima  35021  probmeasb  35112  orvcgteel  35150  orvclteel  35155  ballotlemsima  35198  ballotlemfrceq  35211  ccatmulgnn0dir  35224  fct2relem  35276  ftc2re  35277  chtvalz  35308  subfacp1lem2a  36063  subfaclim  36071  erdsze2lem2  36087  cvmliftlem2  36169  cvmliftlem10  36177  cvmliftlem13  36179  cvmliftiota  36184  cvmlift2lem9  36194  cvmlift2lem11  36196  cvmlift2lem12  36197  cvmliftphtlem  36200  cvmlift3lem6  36207  cvmlift3lem7  36208  cvmlift3lem9  36210  snmlff  36212  mrsubfval  36391  wzel  36710  wsuclem  36711  brsegle  36997  nmulel1  37088  nadddilem1  37093  nadddilem3  37095  opnregcld  37242  weiunfrlem  37376  fin2so  38667  poimirlem17  38692  poimirlem23  38698  opnmbllem0  38711  mblfinlem3  38714  mblfinlem4  38715  itg2addnclem  38726  itg2addnc  38729  itg2gt0cn  38730  ftc1cnnclem  38746  ftc1cnnc  38747  areacirclem5  38767  indexdom  38805  sstotbnd2  38845  isbnd3  38855  isbnd3b  38856  cntotbnd  38867  ismtyima  38874  heibor1lem  38880  heiborlem8  38889  rrncmslem  38903  reheibor  38910  lkrlsp  40296  lshpkrlem5  40308  ldualssvscl  40352  ldualssvsubcl  40353  llnmlplnN  40733  llncvrlpln  40752  pmapjat1  41047  pclfinN  41094  lautlt  41285  lauteq  41289  lautco  41291  ltrn11  41320  ltrnle  41323  ltrneq2  41342  cdlemednuN  41494  cdleme20k  41513  cdleme20l2  41515  cdleme20l  41516  cdleme20m  41517  cdleme21c  41521  cdleme22e  41538  cdleme22eALTN  41539  cdlemefrs32fva  41594  cdlemg4g  41810  cdlemg18b  41873  cdlemg18c  41874  cdlemj3  42017  dia2dimlem5  42262  dvhopN  42310  cdlemm10N  42312  dihjatcclem4  42615  dochexmidlem2  42655  lclkrlem2o  42715  lcfrlem5  42740  lcfrlem6  42741  lcdlssvscl  42800  mapdpglem6  42872  mapdpglem9  42874  mapdpglem12  42877  mapdpglem14  42879  mapdindp0  42913  hdmaprnlem7N  43049  hdmaprnlem8N  43050  hdmaprnlem3eN  43052  hgmapvvlem3  43119  dvun  43547  addinvcom  43620  mzpsubst  43896  eldioph2lem1  43908  eldioph2lem2  43909  eldioph2b  43911  diophin  43920  irrapxlem2  43967  irrapxlem4  43969  irrapxlem5  43970  pellexlem1  43973  pellexlem2  43974  pellexlem6  43978  elpell1qr2  44016  pell1qrgaplem  44017  pell1qrgap  44018  pellqrex  44023  pellfundex  44030  pellfund14  44042  rmspecsqrtnq  44050  rmxyadd  44065  congsub  44114  mzpcong  44116  congrep  44117  acongtr  44122  acongrep  44124  jm2.19lem1  44133  jm2.22  44139  jm2.23  44140  jm2.26lem3  44145  jm2.26  44146  jm2.27a  44149  aomclem6  44198  hbtlem2  44263  hbtlem4  44265  hbtlem5  44267  dgraa0p  44288  rngunsnply  44308  proot1hash  44334  nnoeomeqom  44451  cantnf2  44464  omabs2  44471  naddcnff  44501  naddcnffo  44503  naddcnfcom  44505  naddcnfid1  44506  expgrowth  45456  fpmd  46411  abslt2sqd  46508  ioondisj2  46641  ioondisj1  46642  eliocre  46657  ioossioobi  46665  iooiinicc  46690  iooiinioc  46704  lptioo2  46779  limcresiooub  46788  limsupequzlem  46868  xlimmnfvlem2  46979  xlimpnfvlem2  46983  cncfuni  47032  cncfiooicclem1  47039  cxpcncf2  47045  dvcnre  47062  dvresntr  47064  dvresioo  47067  dvbdfbdioolem1  47074  dvnmptdivc  47084  dvnxpaek  47088  itgsinexplem1  47100  itgcoscmulx  47115  itgiccshift  47126  itgperiod  47127  ovolsplit  47134  stoweidlem11  47157  stoweidlem26  47172  stoweidlem34  47180  stoweidlem36  47182  stoweidlem38  47184  stirlinglem5  47224  dirkercncflem2  47250  dirkercncflem4  47252  fourierdlem20  47273  fourierdlem58  47310  fourierdlem72  47324  fourierdlem73  47325  fourierdlem74  47326  fourierdlem75  47327  fourierdlem76  47328  fourierdlem79  47331  fourierdlem80  47332  fourierdlem87  47339  fourierdlem94  47346  fourierdlem103  47355  fourierdlem104  47356  fourierdlem107  47359  fourierdlem113  47365  sqwvfoura  47374  sqwvfourb  47375  fourierswlem  47376  fouriersw  47377  etransclem46  47426  etransclem47  47427  rrndistlt  47436  rrnprjdstle  47447  ioorrnopnxrlem  47452  sge0ssre  47543  sge0seq  47592  hsphoidmvle2  47731  hsphoidmvle  47732  hoidmv1lelem1  47737  hoidmv1lelem2  47738  hoidmv1lelem3  47739  hoidmvlelem1  47741  hoidifhspdmvle  47766  hoiqssbllem2  47769  ovolval5lem2  47799  iinhoiicc  47820  iunhoiioo  47822  vonioolem2  47827  vonicclem2  47830  issmflem  47873  sqrtnnaa  48049  submodlt  48562  iccpartdisj  48655  m1expevenALTV  48881  fpprel2  48975  tgoldbach  49051  opstrgric  49160  gpg3kgrtriex  49323  nn0eo  49776  fdivpm  49791  refdivpm  49792  elbigolo1  49805  logbpw2m1  49815  fllog2  49816  dignn0flhalflem1  49863  dignn0flhalflem2  49864  itsclinecirc0in  50023  2itscplem2  50027  itscnhlinecirc02plem1  50030  iccdisj2  50147