Theorem syl3anc 1238

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

Hypotheses

Ref	Expression
sylXanc.1	⊢ (𝜑 → 𝜓)
sylXanc.2	⊢ (𝜑 → 𝜒)
sylXanc.3	⊢ (𝜑 → 𝜃)
syl111anc.4	⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syl3anc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3anc

Step	Hyp	Ref	Expression
1		sylXanc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylXanc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylXanc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1177	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl111anc.4	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  syl112anc  1242  syl121anc  1243  syl211anc  1244  syl113anc  1250  syl131anc  1251  syl311anc  1252  syld3an3  1283  3jaod  1304  mpd3an23  1339  stoic4a  1432  rspc3ev  2858  sbciedf  2998  euotd  4252  ordelord  4379  wetriext  4574  releldm  4859  relelrn  4860  f1imass  5770  ovmpodxf  5995  ovmpodf  6001  fovcdmd  6014  offval  6085  caoftrn  6103  offval3  6130  fnmpoovd  6211  tfrlemisucaccv  6321  tfrlemiubacc  6326  tfr1onlemsucaccv  6337  tfr1onlembfn  6340  tfrcllemsucaccv  6350  tfrcllembfn  6353  rdgss  6379  rdgisuc1  6380  rdgisucinc  6381  frecrdg  6404  mapsspm  6677  en2d  6763  en3d  6764  dom3d  6769  ssdomg  6773  f1imaen2g  6788  2dom  6800  cnven  6803  mapen  6841  mapxpen  6843  phpelm  6861  fidifsnen  6865  dif1en  6874  dif1enen  6875  diffisn  6888  isinfinf  6892  unfidisj  6916  unfiin  6920  tpfidisj  6922  xpfi  6924  fisseneq  6926  phpeqd  6927  ssfirab  6928  fnfi  6931  f1dmvrnfibi  6938  iunfidisj  6940  f1finf1o  6941  en1eqsn  6942  fidcenumlemr  6949  updjudhcoinlf  7074  updjudhcoinrg  7075  difinfinf  7095  en2eleq  7189  en2other2  7190  dju1en  7207  djuassen  7211  xpdjuen  7212  addcmpblnq  7361  addassnqg  7376  distrnqg  7381  ltsonq  7392  ltanqg  7394  ltmnqg  7395  ltaddnq  7401  ltexnqq  7402  prarloclemarch  7412  ltrnqg  7414  addcmpblnq0  7437  nnanq0  7452  distrnq0  7453  addassnq0  7456  prarloclemlt  7487  prarloclemcalc  7496  addnqprllem  7521  addnqprulem  7522  addnqprl  7523  addnqpru  7524  addlocprlemgt  7528  appdivnq  7557  prmuloclemcalc  7559  mulnqprl  7562  mulnqpru  7563  mullocprlem  7564  distrlem4prl  7578  distrlem4pru  7579  ltprordil  7583  ltexprlemopl  7595  ltexprlemopu  7597  ltexprlemloc  7601  ltexprlemru  7606  addcanprleml  7608  addcanprlemu  7609  ltaprlem  7612  ltaprg  7613  addextpr  7615  recexprlem1ssu  7628  aptipr  7635  ltmprr  7636  caucvgprlemcanl  7638  cauappcvgprlemopl  7640  cauappcvgprlemdisj  7645  cauappcvgprlemloc  7646  cauappcvgprlemladdfu  7648  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem1  7653  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemloc  7669  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprprlemloccalc  7678  caucvgprprlemml  7688  caucvgprprlemopl  7691  caucvgprprlemloc  7697  caucvgprprlemexb  7701  caucvgprprlemaddq  7702  caucvgprprlem1  7703  caucvgprprlem2  7704  suplocexprlemmu  7712  suplocexprlemru  7713  addcmpblnr  7733  mulcmpblnrlemg  7734  mulcmpblnr  7735  ltsrprg  7741  distrsrg  7753  lttrsr  7756  ltsosr  7758  1idsr  7762  ltasrg  7764  recexgt0sr  7767  mulgt0sr  7772  mulextsr1lem  7774  srpospr  7777  prsradd  7780  prsrlt  7781  caucvgsrlemoffval  7790  caucvgsrlemoffgt1  7793  caucvgsrlemoffres  7794  caucvgsr  7796  ltpsrprg  7797  map2psrprg  7799  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  pitoregt0  7843  recidpirqlemcalc  7851  axmulass  7867  axdistr  7868  rereceu  7883  recriota  7884  addassd  7974  mulassd  7975  adddid  7976  adddird  7977  lelttr  8040  letrd  8075  lelttrd  8076  lttrd  8077  mul12d  8103  mul32d  8104  mul31d  8105  add12d  8118  add32d  8119  cnegexlem3  8128  addcand  8135  addcan2d  8136  pncan  8157  pncan3  8159  subcan2  8176  subsub2  8179  subsub4  8184  npncan3  8189  pnpcan  8190  pnncan  8192  addsub4  8194  subaddd  8280  subadd2d  8281  addsubassd  8282  addsubd  8283  subadd23d  8284  addsub12d  8285  npncand  8286  nppcand  8287  nppcan2d  8288  nppcan3d  8289  subsubd  8290  subsub2d  8291  subsub3d  8292  subsub4d  8293  sub32d  8294  nnncand  8295  nnncan1d  8296  nnncan2d  8297  npncan3d  8298  pnpcand  8299  pnpcan2d  8300  pnncand  8301  ppncand  8302  subcand  8303  subcan2d  8304  subcanad  8305  subcan2ad  8307  subdid  8365  subdird  8366  ltadd2  8370  ltadd2d  8372  ltletrd  8374  ltsubadd  8383  lesubadd  8385  ltaddsub  8387  leaddsub  8389  le2add  8395  lt2add  8396  ltleadd  8397  lesub1  8407  lesub2  8408  ltsub1  8409  ltsub2  8410  lt2sub  8411  le2sub  8412  subge0  8426  lesub0  8430  ltadd1d  8489  leadd1d  8490  leadd2d  8491  ltsubaddd  8492  lesubaddd  8493  ltsubadd2d  8494  lesubadd2d  8495  ltaddsubd  8496  ltaddsub2d  8497  leaddsub2d  8498  subled  8499  lesubd  8500  ltsub23d  8501  ltsub13d  8502  lesub1d  8503  lesub2d  8504  ltsub1d  8505  ltsub2d  8506  gt0add  8524  apcotr  8558  apadd1  8559  addext  8561  mulext1  8563  mulext  8565  gtapd  8588  leltapd  8590  mulap0  8605  mul0eqap  8621  divvalap  8625  divcanap2  8631  diveqap0  8633  divrecap  8639  divassap  8641  divmulassap  8646  divmulasscomap  8647  divdirap  8648  divcanap3  8649  div11ap  8651  rec11ap  8661  divmuldivap  8663  divdivdivap  8664  divmuleqap  8668  dmdcanap  8673  ddcanap  8677  divadddivap  8678  divsubdivap  8679  redivclap  8682  apmul1  8739  divclapd  8741  divcanap1d  8742  divcanap2d  8743  divrecapd  8744  divrecap2d  8745  divcanap3d  8746  divcanap4d  8747  diveqap0d  8748  diveqap1d  8749  diveqap1ad  8750  diveqap0ad  8751  divap0bd  8753  divnegapd  8754  divneg2apd  8755  div2negapd  8756  redivclapd  8786  div2subap  8788  ltmul12a  8811  lemul12b  8812  lt2mul2div  8830  ltdiv2  8838  ltdiv23  8843  avglt1  9151  avglt2  9152  lt2halvesd  9160  div4p1lem1div2  9166  zltp1le  9301  elz2  9318  zdivmul  9337  uztrn  9538  eluzsub  9551  uz3m2nn  9567  qaddcl  9629  elpq  9642  cnref1o  9644  ltdiv2d  9714  lediv2d  9715  divlt1lt  9718  divle1le  9719  ledivge1le  9720  ltmulgt11d  9726  ltmulgt12d  9727  gt0divd  9728  ge0divd  9729  rpgecld  9730  ltmul1d  9732  ltmul2d  9733  lemul1d  9734  lemul2d  9735  ltdiv1d  9736  lediv1d  9737  ltmuldivd  9738  ltmuldiv2d  9739  lemuldivd  9740  lemuldiv2d  9741  ltdivmuld  9742  ltdivmul2d  9743  ledivmuld  9744  ledivmul2d  9745  ltdiv23d  9751  lediv23d  9752  addlelt  9762  xrltso  9790  xrlelttr  9800  xrlttrd  9803  xrlelttrd  9804  xrltletrd  9805  xrletrd  9806  xrre3  9816  xleadd1  9869  xltadd1  9870  xle2add  9873  xlt2add  9874  xlesubadd  9877  xadd4d  9879  ixxss1  9898  ixxss2  9899  ixxss12  9900  iooshf  9946  icoshftf1o  9985  ioodisj  9987  zltaddlt1le  10001  fznlem  10034  fzdifsuc  10074  fzrev  10077  fzrevral2  10099  elfz0fzfz0  10119  elfzmlbp  10125  fzctr  10126  elfzole1  10148  elfzolt2  10149  fzoss2  10165  fzospliti  10169  fzo1fzo0n0  10176  elfzo0z  10177  fzofzim  10181  fzoaddel  10185  eluzgtdifelfzo  10190  elfzodifsumelfzo  10194  ssfzo12bi  10218  elfzonelfzo  10223  fvinim0ffz  10234  rebtwn2zlemstep  10246  rebtwn2z  10248  qbtwnxr  10251  flqge  10275  2tnp1ge0ge0  10294  intfracq  10313  flqdiv  10314  modqval  10317  modqcld  10321  modqmulnn  10335  zmodcl  10337  zmodfz  10339  modqid  10342  zmodid2  10345  modqabs  10350  modqcyc  10352  modqadd1  10354  modqaddabs  10355  modqaddmod  10356  mulp1mod1  10358  modqmuladd  10359  modqmuladdim  10360  modqmuladdnn0  10361  m1modnnsub1  10363  modqltm1p1mod  10369  modqmul1  10370  modqsubmod  10375  modqsubmodmod  10376  q2txmodxeq0  10377  modaddmodup  10380  modqmulmod  10382  modqaddmulmod  10384  modqdi  10385  modqsubdir  10386  addmodlteq  10391  frecuzrdgrrn  10401  frec2uzrdg  10402  frecuzrdgrcl  10403  frecuzrdgsuc  10407  frecuzrdgrclt  10408  frecuzrdgg  10409  frecuzrdgsuctlem  10416  frecfzen2  10420  seq3val  10451  seqvalcd  10452  seqf  10454  seq3p1  10455  seqovcd  10456  seqp1cd  10459  monoord  10469  iseqf1olemqcl  10479  iseqf1olemnab  10481  iseqf1olemmo  10485  iseqf1olemqk  10487  seq3f1olemqsumkj  10491  seq3f1olemstep  10494  expnnval  10516  expnegap0  10521  rpexpcl  10532  expnegzap  10547  expgt1  10551  mulexpzap  10553  exprecap  10554  expaddzaplem  10556  expaddzap  10557  expmul  10558  expmulzap  10559  expdivap  10564  ltexp2a  10565  leexp2a  10566  leexp2r  10567  leexp1a  10568  bernneq2  10634  bernneq3  10635  expnbnd  10636  expnlbnd  10637  expnlbnd2  10638  expaddd  10648  expmuld  10649  expclzapd  10651  expap0d  10652  expnegapd  10653  exprecapd  10654  expp1zapd  10655  expm1apd  10656  sqdivapd  10659  mulexpd  10661  expge0d  10664  expge1d  10665  sqoddm1div8  10666  reexpclzapd  10671  leexp2ad  10675  facwordi  10711  faclbnd3  10714  facavg  10717  bcval  10720  bccmpl  10725  bc0k  10727  bcval5  10734  bcpasc  10737  hashfiv01gt1  10753  hashunlem  10775  hashunsng  10778  fiprsshashgt1  10788  hashdifsn  10790  hashdifpr  10791  hashfz  10792  hashxp  10797  fiubm  10799  hashfacen  10807  zfz1isolemiso  10810  zfz1isolem1  10811  zfz1iso  10812  shftfvalg  10818  seq3shft  10838  mulreap  10864  cjreb  10866  cjap  10906  cnrecnv  10910  cjdivapd  10968  redivapd  10974  imdivapd  10975  resqrexlemdecn  11012  absexpzap  11080  abslt  11088  absle  11089  elicc4abs  11094  abs3lem  11111  fzomaxdiflem  11112  cau3lem  11114  amgm2  11118  abssubge0d  11176  abssuble0d  11177  absdifltd  11178  absdifled  11179  absdivapd  11195  abs3difd  11200  qdenre  11202  maxabslemlub  11207  rexanre  11220  rexico  11221  fimaxre2  11226  lemininf  11233  ltmininf  11234  rpmincl  11237  mul0inf  11240  xrmaxiflemlub  11247  xrmaxltsup  11257  xrmaxaddlem  11259  xrmaxadd  11260  xrltmininf  11269  xrlemininf  11270  xrminltinf  11271  xrminadd  11274  xrbdtri  11275  climshftlemg  11301  climshft2  11305  addcn2  11309  mulcn2  11311  reccn2ap  11312  cn1lem  11313  climadd  11325  climmul  11326  climsub  11327  climsqz  11334  climsqz2  11335  climrecvg1n  11347  climcvg1nlem  11348  fisumss  11391  fsumsplitsn  11409  sumpr  11412  fsumsplitsnun  11418  fsum2dlemstep  11433  fisumcom2  11437  fisum0diag2  11446  fsumconst  11453  modfsummodlemstep  11456  fsumlessfi  11459  fsumabs  11464  fsumiun  11476  hashiun  11477  hash2iun  11478  hash2iun1dif1  11479  binomlem  11482  bcxmas  11488  isumshft  11489  isumlessdc  11495  expcnvap0  11501  expcnvre  11502  geosergap  11505  cvgratnnlembern  11522  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  mertenslemi1  11534  fprodssdc  11589  fprodm1  11597  fprodunsn  11603  fprodeq0  11616  fprod2dlemstep  11621  fprodcom2fi  11625  fprodsplitsn  11632  fprodsplit1f  11633  efaddlem  11673  eftlub  11689  efltim  11697  eirraplem  11775  dvdsval3  11789  nndivdvds  11794  modm1div  11798  summodnegmod  11820  modmulconst  11821  dvds2subd  11825  dvds2addd  11827  dvdstrd  11828  dvdsmultr1d  11830  dvdsmultr2  11831  dvdsabseq  11843  dvdsfac  11856  dvdsmod  11858  oddge22np1  11876  ltoddhalfle  11888  halfleoddlt  11889  nn0ehalf  11898  nno  11901  nn0oddm1d2  11904  divalglemnn  11913  divalg  11919  divalgmod  11922  fldivndvdslt  11930  flodddiv4lt  11931  flodddiv4t2lthalf  11932  infssuzex  11940  dvdsbnd  11947  gcdneg  11973  gcdaddm  11975  modgcd  11982  gcdmultipled  11984  dvdsgcdidd  11985  bezoutlemnewy  11987  bezoutlemstep  11988  bezoutlembi  11996  dvdsgcdb  12004  gcdass  12006  mulgcd  12007  dvdsmulgcd  12016  rpmulgcd  12017  sqgcd  12020  nnwodc  12027  uzwodc  12028  nn0seqcvgd  12031  eucalglt  12047  gcddvdslcm  12063  lcmgcdlem  12067  lcmdvdsb  12074  lcmass  12075  ncoprmgcdne1b  12079  coprmdvds2  12083  mulgcddvds  12084  rpmulgcd2  12085  qredeu  12087  rpdvds  12089  divgcdcoprm0  12091  cncongr1  12093  cncongr2  12094  isprm2lem  12106  prmind2  12110  nprm  12113  dvdsnprmd  12115  exprmfct  12128  prmdvdsfz  12129  isprm5lem  12131  divgcdodd  12133  isprm6  12137  prmdvdsexp  12138  prmexpb  12141  prmfac1  12142  rpexp  12143  rpexp12i  12145  pw2dvdseulemle  12157  sqpweven  12165  2sqpwodd  12166  divnumden  12186  numdensq  12192  nonsq  12197  hashdvds  12211  phiprmpw  12212  crth  12214  phimullem  12215  eulerthlem1  12217  eulerthlemfi  12218  eulerthlemrprm  12219  eulerthlema  12220  eulerthlemh  12221  eulerthlemth  12222  prmdiv  12225  prmdiveq  12226  prmdivdiv  12227  hashgcdlem  12228  phisum  12230  odzdvds  12235  odzphi  12236  vfermltl  12241  powm2modprm  12242  reumodprminv  12243  modprm0  12244  nnnn0modprm0  12245  modprmn0modprm0  12246  coprimeprodsq  12247  pythagtriplem4  12258  pythagtriplem19  12272  pclemub  12277  pcprendvds2  12281  pcpremul  12283  pcval  12286  pcdiv  12292  pcqdiv  12297  pcexp  12299  pcdvdsb  12309  pcidlem  12312  pcdvdstr  12316  pcgcd1  12317  pc2dvds  12319  pcprmpw2  12322  dvdsprmpweqle  12326  pcaddlem  12328  pcadd  12329  pcmpt  12331  pcmptdvds  12333  fldivp1  12336  pcfaclem  12337  pcfac  12338  pcbc  12339  oddprmdvds  12342  prmpwdvds  12343  pockthlem  12344  pockthg  12345  1arith  12355  4sqlem5  12370  4sqlem6  12371  4sqlem7  12372  4sqlem8  12373  4sqlem9  12374  4sqlem4  12380  ennnfonelemp1  12397  ennnfonelemex  12405  ennnfonelemrn  12410  ctinfom  12419  ctiunct  12431  nninfdclemcl  12439  nninfdclemp1  12441  strsetsid  12485  fvsetsid  12486  setsabsd  12491  setscom  12492  ressvalsets  12514  ressex  12515  srngstrd  12594  lmodstrd  12612  ipsstrd  12624  topgrpstrd  12641  plusfvalg  12712  opifismgmdc  12720  mnd4g  12760  mndpfo  12769  mndpropd  12771  issubmnd  12773  mhmf1o  12789  issubmd  12793  mndissubm  12794  mhmco  12802  mhmima  12803  mhmeql  12804  grpcld  12818  grpsubval  12847  grpidssd  12874  grpinvadd  12876  grpsubeq0  12884  grpsubadd  12886  grpsubsub4  12891  dfgrp3m  12897  dfgrp3me  12898  mhmmnd  12908  mulgval  12914  mulgfng  12915  mulg1  12918  mulgnnp1  12919  mulgneg  12929  mulgcld  12932  mulgaddcomlem  12933  mulgaddcom  12934  mulginvcom  12935  mulgz  12938  mulgnndir  12939  mulgnn0dir  12940  mulgdirlem  12941  mulgdir  12942  mulgneg2  12944  mulgass  12947  mulgmodid  12949  mhmmulg  12951  subginv  12967  subgmulg  12974  grpissubg  12980  subgintm  12984  cmn4  13008  rinvmod  13012  ablinvadd  13013  ablsub2inv  13014  ablsub4  13016  abladdsub4  13017  abladdsub  13018  ablpncan3  13020  ablsubsub4  13022  ablpnpcan  13023  ablsub32  13025  ablnnncan  13026  ablnnncan1  13027  ablsubsub23  13028  subcmnd  13029  srgcl  13053  srg1zr  13070  srgmulgass  13072  srgpcomp  13073  srgpcompp  13074  srgpcomppsc  13075  srglmhm  13076  srgrmhm  13077  ringcl  13096  crngcom  13097  ringcom  13114  ringpropd  13117  ringlz  13122  ringnegl  13128  rngnegr  13129  ringmneg1  13130  ringmneg2  13131  ringm2neg  13132  ringsubdi  13133  rngsubdir  13134  mulgass2  13135  ring1  13136  opprvalg  13140  opprring  13148  opprringbg  13149  oppr1g  13151  mulgass3  13153  reldvdsrsrg  13160  dvdsrvald  13161  dvdsrd  13162  dvdsrex  13166  dvdsrtr  13169  dvdsrmul1  13170  opprunitd  13178  unitmulcl  13181  unitgrp  13184  unitnegcl  13198  dvrvald  13202  rdivmuldivd  13212  unitpropdg  13216  ringelnzr  13227  lringuplu  13236  aprsym  13241  aprcotr  13242  difopn  13390  uncld  13395  ntrin  13406  clsss2  13411  ntrcls0  13413  topssnei  13444  neissex  13447  restbasg  13450  tgrest  13451  resttopon  13453  restabs  13457  restopnb  13463  cnpfval  13477  cnprcl2k  13488  tgcnp  13491  iscnp4  13500  cnpnei  13501  cnptopco  13504  cncnpi  13510  cncnp  13512  cnconst2  13515  cnrest  13517  cnrest2  13518  cnrest2r  13519  cnptopresti  13520  cnptoprest  13521  cnptoprest2  13522  lmss  13528  lmtopcnp  13532  txvalex  13536  txval  13537  txbasval  13549  txcnp  13553  txcnmpt  13555  txcn  13557  txdis1cn  13560  lmcn2  13562  cnmptc  13564  cnmpt11  13565  cnmpt1t  13567  cnmpt12  13569  cnmpt21  13573  cnmpt2t  13575  cnmpt22  13576  cnmpt22f  13577  cnmptcom  13580  hmeores  13597  txhmeo  13601  psmettri  13612  xmettri  13654  metrtri  13659  xmetres2  13661  blfvalps  13667  bldisj  13683  blgt0  13684  xblss2ps  13686  xblss2  13687  blhalf  13690  blininf  13706  blssps  13709  blss  13710  blssexps  13711  blssex  13712  blin2  13714  xmeter  13718  blnei  13774  blsscls2  13775  metss2lem  13779  bdmetval  13782  bdxmet  13783  bdbl  13785  xmetxp  13789  xmetxpbl  13790  xmettxlem  13791  xmettx  13792  metcnp3  13793  metcnp  13794  metcnp2  13795  metcnpi  13797  metcnpi2  13798  metcnpi3  13799  txmetcnp  13800  metcnpd  13802  tgqioo  13829  addcncntoplem  13833  fsumcncntop  13838  mulc1cncf  13858  cncfco  13860  mulcncflem  13872  mulcncf  13873  suplociccreex  13884  suplociccex  13885  dedekindicc  13893  ivthinclemlm  13894  ivthinclemum  13895  ivthinclemlopn  13896  ivthinclemuopn  13898  ivthinclemloc  13901  ivthdec  13904  limccl  13910  ellimc3apf  13911  limcimolemlt  13915  cnplimclemle  13919  cnplimclemr  13920  limccnpcntop  13926  limccnp2lem  13927  limccnp2cntop  13928  reldvg  13930  eldvap  13933  dvbssntrcntop  13935  dvcnp2cntop  13945  dvmulxxbr  13948  dvrecap  13959  dveflem  13969  reeff1o  13976  efltlemlt  13977  sin0pilem2  13985  ptolemy  14027  sinq12gt0  14033  cxprec  14113  rpcxproot  14116  cxpmuld  14138  rpabscxpbnd  14141  rplogbval  14145  rplogbchbase  14150  relogbval  14151  relogbzcl  14152  rplogbreexp  14153  rprelogbmul  14155  rprelogbdiv  14157  nnlogbexp  14159  relogbcxpbap  14165  logbgt0b  14166  logbgcd1irr  14167  logbgcd1irraplemexp  14168  logbgcd1irraplemap  14169  logbprmirr  14172  lgslem1  14183  lgslem4  14186  lgsval2lem  14193  lgsvalmod  14202  lgsval4a  14205  lgsneg  14207  lgsmod  14209  lgsdirprm  14217  lgsdir  14218  lgsdilem2  14219  lgsdi  14220  lgsne0  14221  2sqlem2  14233  2sqlem3  14235  2sqlem4  14236  2sqlem6  14238  2sqlem8  14241  apdifflemr  14566  apdiff  14567  iswomni0  14570