MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp1 Unicode version

Theorem simp1 957
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
Assertion
Ref Expression
simp1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )

Proof of Theorem simp1
StepHypRef Expression
1 3simpa 954 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simpld 446 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl1  960  simpr1  963  simp1i  966  simp1d  969  simp11  987  simp21  990  simp31  993  syld3an3  1229  rsp2e  2712  funtpg  5441  feq123  5524  fresaun  5554  foco2  5828  ftpg  5855  fsnunf  5870  fsnunf2  5871  fnsuppres  5891  fcofo  5960  fveqf1o  5968  f1oiso2  6011  ovmpt2x  6141  ovmpt2ga  6142  ofeq  6246  ofrval  6254  riotass  6514  riotasv2s  6532  onoviun  6541  omwordri  6751  omeulem1  6761  oeord  6767  oewordri  6771  oeordsuc  6773  erov  6937  mapxpen  7209  unbnn  7299  fofinf1o  7323  elfir  7355  inelfi  7358  dffi2  7363  elfiun  7370  fisup2g  7404  suppr  7406  ordtype2  7436  hartogslem1  7444  wemapso  7453  wemapso2  7454  ixpiunwdom  7492  cnfcom3clem  7595  cdaassen  7995  mapcdaen  7997  infcdaabs  8019  infunabs  8020  infdif  8022  infdif2  8023  cfsmolem  8083  isf32lem11  8176  isf34lem7  8192  zornn0g  8318  ttukey2g  8329  konigthlem  8376  gchdomtri  8437  fpwwe  8454  canthwe  8459  gchaleph  8483  gchaleph2  8484  winainflem  8501  wununi  8514  tsksuc  8570  tskpr  8578  tskop  8579  tskcard  8589  grupw  8603  grurn  8609  gruop  8613  gruun  8614  grumap  8616  gruixp  8617  distrlem4pr  8836  ltadd2  9110  mul31  9166  readdcan  9172  addid2  9181  addsubass  9247  subcan2  9258  subsub2  9261  subsub4  9266  npncan3  9271  pnpcan  9272  pnncan  9274  subcan  9288  subdi  9399  ltadd1  9427  leadd1  9428  leadd2  9429  ltsubadd  9430  lesubadd  9432  lesub1  9454  lesub2  9455  ltsub1  9456  ltsub2  9457  mulcan  9591  mulcan2  9592  divcan2  9618  diveq0  9620  divrec  9626  divrec2  9627  divdir  9633  divcan3  9634  div11  9636  divcan5  9648  redivcl  9665  div2neg  9669  ltmul1  9792  ltdiv1  9806  ltmuldiv  9812  ledivmulOLD  9816  lemuldiv  9821  lt2msq1  9825  suprub  9901  suprlub  9902  infmsup  9918  infmrgelb  9920  infmrlb  9921  ofsubeq0  9929  ofnegsub  9930  ofsubge0  9931  gtndiv  10279  eluz2  10426  peano2uz  10462  suprzub  10499  xrltmin  10702  xrlemin  10704  xaddass  10760  xleadd1  10766  xltadd1  10767  xmulass  10798  xlemul1  10801  xlemul2  10802  xltmul1  10803  xadddi  10806  xadddir  10807  xadddi2  10808  supxrre  10838  infmxrre  10846  ixxssixx  10862  ixxub  10869  ixxlb  10870  lbico1  10898  lbicc2  10945  icoshftf1o  10952  snunioo  10955  snunico  10956  iccsplit  10961  fzrev3  11042  fzm1  11057  fzrevral2  11062  elfzo0  11101  flwordi  11146  flword2  11147  expgt1  11345  exprec  11348  leexp2a  11362  expubnd  11367  sqdiv  11374  expnbnd  11435  expmulnbnd  11438  modexp  11441  bccmpl  11527  ccatass  11677  swrdval  11691  swrdval2  11694  ccatco  11731  s3cl  11768  swrds2  11807  mulre  11853  caubnd  12089  climuni  12273  iseraltlem3  12404  geoisum1c  12584  eflt  12645  rpnnen2lem4  12744  dvdsmultr2  12812  dvdsexp  12832  sadass  12910  dvdsgcdb  12971  gcdass  12972  mulgcd  12973  gcddiv  12976  rplpwr  12983  coprmdvds  13029  mulgcddvds  13031  qredeq  13033  rpexp12i  13049  rpmul  13050  odzcllem  13105  odzphi  13109  pythagtriplem15  13130  pcpremul  13144  pcdiv  13153  pcqmul  13154  pcqdiv  13158  vdwapfval  13266  vdwapun  13269  vdwpc  13275  hashbcss  13299  ramval  13303  0ram2  13316  0ramcl  13318  ramcl  13324  ressbas  13446  xpsadd  13728  xpsmul  13729  mreiincl  13748  mreincl  13751  mrcss  13768  mrcun  13774  submrc  13780  posasymb  14336  meetle  14384  p0le  14399  ple1  14400  latleeqj1  14419  latjlej12  14423  latleeqm1  14435  latmlem12  14439  latnlemlt  14440  latj4  14457  latj4rot  14458  lubss  14475  lubun  14477  clatglbss  14481  pospropd  14488  isipodrs  14514  imasmnd2  14659  gsumccat  14714  frmdup3  14738  grpinvadd  14794  grpsubeq0  14802  grppncan  14806  grpsubpropd2  14817  pwsinvg  14857  imasgrp2  14860  issubg  14871  nsgconj  14900  nsgid  14913  ghmnsgima  14956  odcong  15114  isslw  15169  pgpssslw  15175  lsmsubg  15215  efgsval2  15292  frgpup3  15337  cmn4  15358  ablinvadd  15361  ablsub4  15364  abladdsub4  15365  ablpncan2  15367  lsmsubg2  15401  lsm4  15402  rngcom  15619  imasrng  15652  unitmulcl  15696  unitmulclb  15697  dvrcan1  15723  dvrcan3  15724  irredrmul  15739  isabvd  15835  abvdom  15853  islmod  15881  lmodcom  15917  lss0cl  15950  lssvnegcl  15959  lssincl  15968  lspss  15987  lspun  15990  lspsnvsi  16007  lsslsp  16018  lmodvsinv  16039  lmodvsinv2  16040  0lmhm  16043  lsmsp  16085  lsmsp2  16086  lspvadd  16095  lspsntri  16096  lidldvgen  16253  rrgeq0  16277  aspid  16316  aspss  16318  asclmul1  16325  asclmul2  16326  psrbagaddcl  16362  psrbagconcl  16365  coe1tm  16592  coe1sclmul  16601  coe1sclmul2  16603  phllmhm  16786  ip2eq  16807  cssmre  16843  iuncld  17032  clsss  17041  ntrin  17048  clsndisj  17062  iscldtop  17082  neiss  17096  lpss3  17131  restco  17150  restabs  17151  restcldi  17159  neitr  17166  restcls  17167  restntr  17168  restlp  17169  lmconst  17247  cnpresti  17274  hausnei2  17339  sshauslem  17358  clscon  17414  concompss  17417  concompclo  17419  kgen2ss  17508  elptr  17526  xkococn  17613  qtopval2  17649  qtoptop2  17652  cmphaushmeo  17753  elmptrab  17780  filinn0  17813  fbasweak  17818  snfbas  17819  filuni  17838  trnei  17845  fmval  17896  rnelfm  17906  flimrest  17936  flimclslem  17937  flfnei  17944  isflf  17946  lmflf  17958  fclsneii  17970  fclsrest  17977  isfcf  17987  ptcmpg  18009  istgp2  18042  divstgpopn  18070  divstgphaus  18073  ustfn  18152  ustval  18153  isust  18154  ustssel  18156  ustn0  18171  trust  18180  utop2nei  18201  ressusp  18216  trcfilu  18245  cfiluweak  18246  xmetge0  18283  xmetsym  18286  xmetresbl  18357  mopni3  18414  stdbdxmet  18435  stdbdmopn  18438  prdsxms  18450  prdsms  18451  metustbl  18486  xmsusp  18488  restmetu  18489  isngp4  18529  nmsub  18540  nm2dif  18542  nminvr  18576  nmoix  18634  nmods  18649  metds0  18751  metnrm  18763  cncfmptc  18812  iirev  18825  icoopnst  18835  iocopnst  18836  icchmeo  18837  iccpnfhmeo  18841  pi1blem  18935  isclmi  18973  cphsqrcl  19018  cph2ass  19046  ipcau  19066  nmpar  19068  fmcfil  19096  iscau3  19102  cmetcaulem  19112  cfilres  19120  bcthlem1  19146  bcthlem5  19150  cncdrg  19180  rlmbn  19182  cniccbdd  19225  ovolunnul  19263  ovolicc  19286  iundisj2  19310  ovolioo  19329  volcn  19365  itg1le  19472  itg2le  19498  iblcnlem  19547  dvfval  19651  dvid  19671  dvcnp2  19673  dvnf  19680  dvnbss  19681  dvn2bss  19683  evlsval2  19808  tdeglem3  19849  mdegldg  19856  mdegmullem  19868  deg1ldgdomn  19884  deg1lt  19887  deg1scl  19903  deg1mul3  19905  q1peqb  19944  fta1b  19959  elplyr  19987  ply1term  19990  dgrub  20020  coe1term  20044  dgradd2  20053  dgrmulc  20056  ofmulrt  20066  quotcl2  20086  quotdgr  20087  facth  20090  quotcan  20093  aannenlem1  20112  aannenlem2  20113  ulmf  20165  ptolemy  20271  tanord1  20306  efif1o  20315  argrege0  20373  logimul  20376  cxpneg  20439  ang180lem1  20518  ang180lem2  20519  ang180lem3  20520  ang180lem4  20521  isosctrlem2  20530  cxp2lim  20682  amgmlem  20695  wilthlem3  20720  sgmppw  20848  lgslem1  20947  lgsneg  20970  lgssq2  20987  lgsdirnn0  20990  lgsqrlem5  20996  lgsquad  21008  dirith  21090  pntrmax  21125  qrngdiv  21185  padicabv  21191  pthistrl  21426  1pthon  21439  2pthonlem2  21448  grpoasscan2  21674  grpoinvop  21677  grpopncan  21687  grponpcan  21688  grpopnpcan2  21689  gxneg  21702  gxneg2  21703  gxcom  21705  gxinv  21706  gxsuc  21708  gxadd  21711  gxnn0mul  21713  gxmul  21714  gxmodid  21715  rngoass  21823  rngosn  21840  zerdivemp1  21870  nvpncan2  21985  nvaddsub4  21990  nvnncan  21992  nvdif  22002  nvpi  22003  nvz  22006  nvabs  22010  nv1  22013  imsmetlem  22030  4ipval2  22052  lnoadd  22107  isblo3i  22150  hvsubass  22394  shlub  22764  homco2  23328  leopmul2i  23486  mdslmd4i  23684  atexch  23732  atcvatlem  23736  cdj3lem2  23786  cdj3lem2a  23787  iundisj2f  23873  curry2ima  23938  supxrnemnf  23963  snunioc  23973  ubico  23974  iundisj2fi  23991  divnumden2  23999  xreceu  24006  xdivcl  24008  xdivrec  24011  xrge0addass  24040  ofldaddlt  24067  rhmdvd  24075  redvr  24093  cnre2csqlem  24112  relogbcl  24198  logb1  24199  logblt  24202  hasheuni  24271  sigaclcuni  24297  difelsiga  24312  elsigagen2  24327  sigagenss2  24329  measbase  24347  measval  24348  ismeas  24349  isrnmeas  24350  measxun2  24358  measun  24359  measvunilem  24360  measvuni  24362  mbfmco2  24409  dya2iocnrect  24425  probun  24456  probdif  24457  totprob  24464  probmeasb  24467  cndprobin  24471  cndprobnul  24474  ballotlemfrcn0  24566  erdszelem2  24657  cvmcov2  24741  dedekindle  24967  mulcan1g  24968  subdivcomb1  24974  dfon2lem2  25164  frrlem3  25307  brbtwn  25552  brbtwn2  25558  colinearalglem1  25559  colinearalglem2  25560  colinearalg  25563  axcgrid  25569  ax5seglem1  25581  ax5seglem2  25582  axpasch  25594  axlowdimlem16  25610  axcontlem4  25620  axcontlem7  25623  cgrrflx  25635  cgrcomim  25637  cgrtr  25640  cgrtr3  25642  cgrcoml  25644  cgrcomr  25645  cgrtriv  25650  cgrdegen  25652  cgrextend  25656  segconeq  25658  segconeu  25659  btwntriv2  25660  btwntriv1  25664  btwnintr  25667  btwnexch3  25668  btwnouttr2  25670  btwnouttr  25672  btwnexch  25673  funtransport  25679  btwnxfr  25704  colinearex  25708  colineartriv1  25715  colineartriv2  25716  colinearxfr  25723  lineext  25724  linecgr  25729  lineid  25731  idinside  25732  btwnconn1lem7  25741  btwnconn1lem8  25742  btwnconn1lem9  25743  btwnconn1lem12  25746  btwnconn1lem14  25748  btwnconn3  25751  midofsegid  25752  segcon2  25753  seglerflx  25760  segletr  25762  outsidene1  25771  btwnoutside  25773  broutsideof3  25774  outsideoftr  25777  outsideofeq  25778  funray  25788  liness  25793  lineunray  25795  lineelsb2  25796  linecom  25798  linethru  25801  hilbert1.1  25802  bpolycl  25812  bpolydif  25815  areacirclem4  25984  areacirclem6  25987  areacirc  25988  elicc3  26011  clsun  26022  neiin  26026  finlocfin  26070  blbnd  26187  zerdivemp1x  26262  smprngopr  26353  isfldidl  26369  istopclsd  26445  ismrc  26446  mapco2g  26460  mapfzcons  26463  ofmpteq  26467  mzpcl34  26479  mzpexpmpt  26493  mzpsubst  26496  mzpresrename  26498  eldioph  26507  diophrw  26508  eqrabdioph  26527  lerabdioph  26556  ltrabdioph  26559  dvdsrabdioph  26561  diophren  26565  pellex  26589  pell14qrexpclnn0  26620  pellfundex  26640  rmxyadd  26675  rmyabs  26714  jm2.17a  26716  mzpcong  26728  acongeq  26739  coprmdvdsb  26743  modabsdifz  26747  jm2.22  26757  jm2.20nn  26759  rmxdiophlem  26777  rmxdioph  26778  jm3.1  26782  expdiophlem2  26784  islssfgi  26839  pwssplit0  26856  pwssplit1  26857  pwssplit2  26858  pwssplit3  26859  pwssplit4  26860  uvcresum  26911  frlmsplit2  26912  frlmsslss  26913  frlmup4  26922  islindf2  26953  lindsind2  26958  lindff1  26959  f1lindf  26961  lindsss  26963  f1linds  26964  cnsrexpcl  27039  pmtrfrn  27069  idomrootle  27180  fiuneneq  27182  ofdivrec  27212  ofdivcan4  27213  ubelsupr  27359  fnchoice  27368  fmul01  27378  fmuldfeq  27381  fmul01lt1lem2  27383  infrglb  27390  climsuse  27402  stoweidlem16  27433  stoweidlem20  27437  stoweidlem60  27477  wallispilem3  27484  sigaraf  27511  sigarmf  27512  sigaras  27513  sigarms  27514  sigarls  27515  sigarperm  27518  3orbi123  27937  alrim3con13v  27960  tratrb  27963  3orbi123VD  28303  19.21a3con13vVD  28305  tratrbVD  28314  bnj900  28638  bnj1110  28689  bnj1128  28697  bnj1125  28699  bnj1136  28704  bnj1189  28716  bnj1204  28719  bnj1321  28734  bnj1413  28742  lubunNEW  29088  lfladd  29181  lflsub  29182  lflmul  29183  lkrlsp2  29218  lshpkrlem5  29229  oplecon3b  29315  latm4  29348  omllaw4  29361  omllaw5N  29362  cmtcomlemN  29363  cmtbr2N  29368  cmtbr3N  29369  omlmod1i2N  29375  omlspjN  29376  cvrnbtwn3  29391  cvrcon3b  29392  cvrcmp  29398  cvrcmp2  29399  cvlatexch3  29453  cvlsupr5  29461  cvlsupr7  29463  hlrelat2  29517  2llnneN  29523  cvrval5  29529  cvrexch  29534  cvratlem  29535  atcvr0eq  29540  atcvrneN  29544  atcvrj1  29545  atle  29550  atlt  29551  atlelt  29552  2atjm  29559  3noncolr2  29563  3noncolr1N  29564  hlatcon2  29566  3dim1  29581  3dim2  29582  1cvratex  29587  1cvrat  29590  ps-1  29591  ps-2  29592  2atjlej  29593  hlatexch3N  29594  llnexatN  29635  llncmp  29636  lplni2  29651  lplnnle2at  29655  lplnnleat  29656  lplnri3N  29669  2lplnmN  29673  2llnmj  29674  lplncmp  29676  lplnexatN  29677  2llnm2N  29682  2llnm3N  29683  2llnmeqat  29685  2atnelvolN  29701  4atlem0ae  29708  4atlem0be  29709  4atlem3b  29712  4atlem9  29717  4atlem10a  29718  4atlem10  29720  lvolcmp  29731  2lplnm2N  29735  2lplnmj  29736  pmapglbx  29883  pmapmeet  29887  2llnma1b  29900  2llnma1  29901  2llnma3r  29902  2llnma2  29903  2llnma2rN  29904  elpadd2at  29920  paddasslem16  29949  padd4N  29954  paddclN  29956  pmodlem2  29961  pmapjoin  29966  pmapjat1  29967  pmapjat2  29968  hlmod1i  29970  atmod2i1  29975  atmod2i2  29976  atmod3i1  29978  llnexchb2  29983  dalawlem2  29986  elpcliN  30007  pclssN  30008  pclunN  30012  pclun2N  30013  polcon3N  30031  2polcon4bN  30032  paddunN  30041  poldmj1N  30042  pmapj2N  30043  pmapocjN  30044  psubclinN  30062  paddatclN  30063  poml5N  30068  osumcllem3N  30072  pexmidlem3N  30086  pexmidlem4N  30087  lhple  30156  lhpat4N  30158  4atex2  30191  4atex2-0bOLDN  30193  4atex3  30195  ltrnatb  30251  ltrnel  30253  ltrncnvel  30256  ltrncoelN  30257  ltrncoat  30258  ltrncoval  30259  ltrncnv  30260  ltrn11at  30261  ltrnmw  30265  trlcnv  30279  trljat2  30281  trlat  30283  trl0  30284  ltrnnidn  30288  trlnid  30293  trlval3  30301  trlval4  30302  cdlemc2  30306  cdlemc5  30309  cdlemc6  30310  cdlemd7  30318  cdleme00a  30323  cdleme0e  30331  cdleme01N  30335  cdleme02N  30336  cdleme0ex1N  30337  cdleme0ex2N  30338  cdleme3g  30348  cdleme3h  30349  cdleme3  30351  cdleme4  30352  cdleme5  30354  cdleme7b  30358  cdleme9  30367  cdleme11a  30374  cdleme11dN  30376  cdleme11e  30377  cdleme11g  30379  cdleme11h  30380  cdleme11j  30381  cdleme11k  30382  cdleme12  30385  cdleme18a  30405  cdleme18b  30406  cdleme18c  30407  cdleme22gb  30408  cdleme20zN  30415  cdleme20y  30416  cdleme19a  30417  cdleme20d  30426  cdleme20i  30431  cdleme20j  30432  cdleme20l2  30435  cdleme22a  30454  cdleme22d  30457  cdleme22e  30458  cdleme30a  30492  cdlemefs32sn1aw  30528  cdlemefs29bpre0N  30530  cdlemefs29bpre1N  30531  cdlemefs29cpre1N  30532  cdlemefs29clN  30533  cdleme43fsv1snlem  30534  cdlemefs32fvaN  30536  cdlemefs32fva1  30537  cdlemefs31fv1  30538  cdlemefs45eN  30545  cdleme41sn3a  30547  cdleme32fva  30551  cdleme32fvaw  30553  cdleme32b  30556  cdleme32c  30557  cdleme32e  30559  cdleme35h  30570  cdleme37m  30576  cdleme38m  30577  cdleme40m  30581  cdleme40n  30582  cdleme41sn3aw  30588  cdleme41sn4aw  30589  cdleme41fva11  30591  cdleme42b  30592  cdleme42e  30593  cdleme42h  30596  cdleme42i  30597  cdleme42k  30598  cdleme43cN  30605  cdleme17d2  30609  cdleme17d3  30610  cdleme48fv  30613  cdleme48bw  30616  cdleme48b  30617  cdlemeg47rv2  30624  cdlemeg46c  30627  cdlemeg46sfg  30634  cdlemeg46fjgN  30635  cdlemeg46rjgN  30636  cdlemeg46fjv  30637  cdlemeg46frv  30639  cdlemeg46vrg  30641  cdlemeg46rgv  30642  cdlemeg46req  30643  cdlemeg46gfv  30644  cdlemeg46gfre  30646  cdleme48d  30649  cdlemeg49lebilem  30653  cdleme50trn2  30665  cdleme50ltrn  30671  ltrniotacnvval  30696  ltrniotavalbN  30698  cdlemg1cex  30702  cdlemg2dN  30704  cdlemg2fvlem  30708  cdlemg2fv2  30714  cdlemg2kq  30716  cdlemg2l  30717  cdlemg2m  30718  cdlemg4a  30722  cdlemg4b1  30723  cdlemg4b2  30724  cdlemg4d  30727  cdlemg4e  30728  cdlemg4f  30729  cdlemg4  30731  cdlemg6d  30735  cdlemg6e  30736  cdlemg7fvN  30738  cdlemg8a  30741  cdlemg8b  30742  cdlemg8c  30743  cdlemg9a  30746  cdlemg9b  30747  cdlemg9  30748  cdlemg11aq  30752  cdlemg10c  30753  cdlemg12a  30757  cdlemg12b  30758  cdlemg12c  30759  cdlemg12f  30762  cdlemg12g  30763  cdlemg14f  30767  cdlemg14g  30768  cdlemg17a  30775  cdlemg17dN  30777  cdlemg17e  30779  cdlemg17i  30783  cdlemg17ir  30784  cdlemg17  30791  cdlemg18b  30793  cdlemg18c  30794  cdlemg18d  30795  cdlemg18  30796  cdlemg21  30800  cdlemg28a  30807  cdlemg31b0a  30809  cdlemg31a  30811  cdlemg31b  30812  cdlemg28b  30817  cdlemg33c  30822  cdlemg33d  30823  cdlemg33e  30824  cdlemg35  30827  cdlemg41  30832  ltrnco  30833  trlcocnv  30834  trlcoabs  30835  trlcoabs2N  30836  trlcocnvat  30838  trlconid  30839  trlcolem  30840  trlcone  30842  cdlemg42  30843  cdlemg43  30844  cdlemg44a  30845  cdlemg47a  30848  cdlemg46  30849  trljco  30854  tendoset  30873  tendof  30877  tendoeq1  30878  tendocoval  30880  tendoco2  30882  tendococl  30886  tendoplcl2  30892  tendoplco2  30893  tendopltp  30894  tendoplcl  30895  tendoplcom  30896  cdlemh  30931  cdlemi1  30932  cdlemi2  30933  cdlemk1  30945  cdlemk2  30946  cdlemk3  30947  cdlemk4  30948  cdlemk8  30952  cdlemk9  30953  cdlemk9bN  30954  cdlemki  30955  cdlemkvcl  30956  cdlemk10  30957  cdlemksv2  30961  cdlemk7  30962  cdlemk11  30963  cdlemk12  30964  cdlemk5u  30975  cdlemk6u  30976  cdlemk7u  30984  cdlemk12u  30986  cdlemk22  31007  cdlemk32  31011  cdlemk28-3  31022  cdlemk34  31024  cdlemk29-3  31025  cdlemk39  31030  cdlemkfid1N  31035  cdlemkid1  31036  cdlemkid2  31038  cdlemkfid3N  31039  cdlemk54  31072  cdlemk19u  31084  cdlemk56w  31087  tendoex  31089  cdleml1N  31090  cdleml2N  31091  cdleml3N  31092  cdleml6  31095  cdleml7  31096  cdleml8  31097  cdleml9  31098  tendocnv  31136  tendospcanN  31138  dvhopvadd  31208  tendolinv  31220  tendorinv  31221  dicvaddcl  31305  dicvscacl  31306  cdlemn2  31310  cdlemn2a  31311  cdlemn3  31312  cdlemn4  31313  cdlemn4a  31314  cdlemn5pre  31315  cdlemn6  31317  cdlemn7  31318  cdlemn8  31319  cdlemn9  31320  cdlemn10  31321  cdlemn11a  31322  cdlemn11c  31324  cdlemn11pre  31325  dihordlem6  31328  dihordlem7  31329  dihordlem7b  31330  dihjustlem  31331  dihjust  31332  dihord2cN  31336  dihord11c  31339  dihvalcq2  31362  dihopelvalcpre  31363  dihmeetlem1N  31405  dihglblem3N  31410  dihmeetlem2N  31414  dihglbcpreN  31415  dihmeetcN  31417  dihmeetbclemN  31419  dihmeetlem4preN  31421  dihmeetlem9N  31430  dihmeetlem13N  31434  dihmeetlem20N  31441  dih1dimatlem0  31443  dihlspsnat  31448  dihmeet  31458  dochss  31480  dochdmj1  31505  hdmap1fval  31912  hdmapfval  31945  hgmapfval  32004
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator