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  intn3an1d  1293  rsp2e  2756  funtpg  5487  feq123  5570  fresaun  5600  foco2  5875  ftpg  5902  fsnunf  5917  fsnunf2  5918  fnsuppres  5938  fcofo  6007  fveqf1o  6015  f1oiso2  6058  ovmpt2x  6188  ovmpt2ga  6189  ofeq  6293  ofrval  6301  riotass  6564  riotasv2s  6582  onoviun  6591  omwordri  6801  omeulem1  6811  oeord  6817  oewordri  6821  oeordsuc  6823  erov  6987  mapxpen  7259  unbnn  7349  fofinf1o  7373  elfir  7406  inelfi  7409  dffi2  7414  elfiun  7421  fisup2g  7455  suppr  7457  ordtype2  7487  hartogslem1  7495  wemapso  7504  wemapso2  7505  ixpiunwdom  7543  cnfcom3clem  7646  cdaassen  8046  mapcdaen  8048  infcdaabs  8070  infunabs  8071  infdif  8073  infdif2  8074  cfsmolem  8134  isf32lem11  8227  isf34lem7  8243  zornn0g  8369  ttukey2g  8380  konigthlem  8427  gchdomtri  8488  fpwwe  8505  canthwe  8510  gchaleph  8534  gchaleph2  8535  winainflem  8552  wununi  8565  tsksuc  8621  tskpr  8629  tskop  8630  tskcard  8640  grupw  8654  grurn  8660  gruop  8664  gruun  8665  grumap  8667  gruixp  8668  distrlem4pr  8887  ltadd2  9161  mul31  9218  readdcan  9224  addid2  9233  addsubass  9299  subcan2  9310  subsub2  9313  subsub4  9318  npncan3  9323  pnpcan  9324  pnncan  9326  subcan  9340  subdi  9451  ltadd1  9479  leadd1  9480  leadd2  9481  ltsubadd  9482  lesubadd  9484  lesub1  9506  lesub2  9507  ltsub1  9508  ltsub2  9509  mulcan  9643  mulcan2  9644  divcan2  9670  diveq0  9672  divrec  9678  divrec2  9679  divdir  9685  divcan3  9686  div11  9688  divcan5  9700  redivcl  9717  div2neg  9721  ltmul1  9844  ltdiv1  9858  ltmuldiv  9864  ledivmulOLD  9868  lemuldiv  9873  lt2msq1  9877  suprub  9953  suprlub  9954  infmsup  9970  infmrgelb  9972  infmrlb  9973  ofsubeq0  9981  ofnegsub  9982  ofsubge0  9983  gtndiv  10331  eluz2  10478  peano2uz  10514  suprzub  10551  xrltmin  10754  xrlemin  10756  xaddass  10812  xleadd1  10818  xltadd1  10819  xmulass  10850  xlemul1  10853  xlemul2  10854  xltmul1  10855  xadddi  10858  xadddir  10859  xadddi2  10860  supxrre  10890  infmxrre  10898  ixxssixx  10914  ixxub  10921  ixxlb  10922  lbico1  10950  lbicc2  10997  icoshftf1o  11004  snunioo  11007  snunico  11008  iccsplit  11013  fzrev3  11095  fzm1  11110  fzrevral2  11115  elfzo0  11154  flwordi  11202  flword2  11203  expgt1  11401  exprec  11404  leexp2a  11418  expubnd  11423  sqdiv  11430  expnbnd  11491  expmulnbnd  11494  modexp  11497  bccmpl  11583  ccatass  11733  swrdval  11747  swrdval2  11750  ccatco  11787  s3cl  11824  swrds2  11863  mulre  11909  caubnd  12145  climuni  12329  iseraltlem3  12460  geoisum1c  12640  eflt  12701  rpnnen2lem4  12800  dvdsmultr2  12868  dvdsexp  12888  sadass  12966  dvdsgcdb  13027  gcdass  13028  mulgcd  13029  gcddiv  13032  rplpwr  13039  coprmdvds  13085  mulgcddvds  13087  qredeq  13089  rpexp12i  13105  rpmul  13106  odzcllem  13161  odzphi  13165  pythagtriplem15  13186  pcpremul  13200  pcdiv  13209  pcqmul  13210  pcqdiv  13214  vdwapfval  13322  vdwapun  13325  vdwpc  13331  hashbcss  13355  ramval  13359  0ram2  13372  0ramcl  13374  ramcl  13380  ressbas  13502  xpsadd  13784  xpsmul  13785  mreiincl  13804  mreincl  13807  mrcss  13824  mrcun  13830  submrc  13836  posasymb  14392  meetle  14440  p0le  14455  ple1  14456  latleeqj1  14475  latjlej12  14479  latleeqm1  14491  latmlem12  14495  latnlemlt  14496  latj4  14513  latj4rot  14514  lubss  14531  lubun  14533  clatglbss  14537  pospropd  14544  isipodrs  14570  imasmnd2  14715  gsumccat  14770  frmdup3  14794  grpinvadd  14850  grpsubeq0  14858  grppncan  14862  grpsubpropd2  14873  pwsinvg  14913  imasgrp2  14916  issubg  14927  nsgconj  14956  nsgid  14969  ghmnsgima  15012  odcong  15170  isslw  15225  pgpssslw  15231  lsmsubg  15271  efgsval2  15348  frgpup3  15393  cmn4  15414  ablinvadd  15417  ablsub4  15420  abladdsub4  15421  ablpncan2  15423  lsmsubg2  15457  lsm4  15458  rngcom  15675  imasrng  15708  unitmulcl  15752  unitmulclb  15753  dvrcan1  15779  dvrcan3  15780  irredrmul  15795  isabvd  15891  abvdom  15909  islmod  15937  lmodcom  15973  lss0cl  16006  lssvnegcl  16015  lssincl  16024  lspss  16043  lspun  16046  lspsnvsi  16063  lsslsp  16074  lmodvsinv  16095  lmodvsinv2  16096  0lmhm  16099  lsmsp  16141  lsmsp2  16142  lspvadd  16151  lspsntri  16152  lidldvgen  16309  rrgeq0  16333  aspid  16372  aspss  16374  asclmul1  16381  asclmul2  16382  psrbagaddcl  16418  psrbagconcl  16421  coe1tm  16648  coe1sclmul  16657  coe1sclmul2  16659  phllmhm  16846  ip2eq  16867  cssmre  16903  iuncld  17092  clsss  17101  ntrin  17108  clsndisj  17122  iscldtop  17142  neiss  17156  lpss3  17191  restco  17211  restabs  17212  restcldi  17220  neitr  17227  restcls  17228  restntr  17229  restlp  17230  lmconst  17308  cnpresti  17335  hausnei2  17400  sshauslem  17419  bwth  17456  clscon  17476  concompss  17479  concompclo  17481  kgen2ss  17570  elptr  17588  xkococn  17675  qtopval2  17711  qtoptop2  17714  cmphaushmeo  17815  elmptrab  17842  filinn0  17875  fbasweak  17880  snfbas  17881  filuni  17900  trnei  17907  fmval  17958  rnelfm  17968  flimrest  17998  flimclslem  17999  flfnei  18006  isflf  18008  lmflf  18020  fclsneii  18032  fclsrest  18039  isfcf  18049  ptcmpg  18071  istgp2  18104  divstgpopn  18132  divstgphaus  18135  ustfn  18214  ustval  18215  isust  18216  ustssel  18218  ustn0  18233  trust  18242  utop2nei  18263  ressusp  18278  trcfilu  18307  cfiluweak  18308  psmetsym  18324  psmetge0  18326  xmetge0  18357  xmetsym  18360  xmetresbl  18450  mopni3  18507  stdbdxmet  18528  stdbdmopn  18531  prdsxms  18543  prdsms  18544  metustblOLD  18593  metustbl  18594  xmsuspOLD  18598  xmsusp  18599  restmetu  18600  isngp4  18641  nmsub  18652  nm2dif  18654  nminvr  18688  nmoix  18746  nmods  18761  metds0  18863  metnrm  18875  cncfmptc  18924  iirev  18937  icoopnst  18947  iocopnst  18948  icchmeo  18949  iccpnfhmeo  18953  pi1blem  19047  isclmi  19085  cphsqrcl  19130  cph2ass  19158  ipcau  19178  nmpar  19180  fmcfil  19208  iscau3  19214  cmetcaulem  19224  cfilres  19232  bcthlem1  19260  bcthlem5  19264  cncdrg  19296  rlmbn  19298  cniccbdd  19341  ovolunnul  19379  ovolicc  19402  iundisj2  19426  ovolioo  19445  volcn  19481  itg1le  19588  itg2le  19614  iblcnlem  19663  dvfval  19767  dvid  19787  dvcnp2  19789  dvnf  19796  dvnbss  19797  dvn2bss  19799  evlsval2  19924  tdeglem3  19965  mdegldg  19972  mdegmullem  19984  deg1ldgdomn  20000  deg1lt  20003  deg1scl  20019  deg1mul3  20021  q1peqb  20060  fta1b  20075  elplyr  20103  ply1term  20106  dgrub  20136  coe1term  20160  dgradd2  20169  dgrmulc  20172  ofmulrt  20182  quotcl2  20202  quotdgr  20203  facth  20206  quotcan  20209  aannenlem1  20228  aannenlem2  20229  ulmf  20281  ptolemy  20387  tanord1  20422  efif1o  20431  argrege0  20489  logimul  20492  cxpneg  20555  ang180lem1  20634  ang180lem2  20635  ang180lem3  20636  ang180lem4  20637  isosctrlem2  20646  cxp2lim  20798  amgmlem  20811  wilthlem3  20836  sgmppw  20964  lgslem1  21063  lgsneg  21086  lgssq2  21103  lgsdirnn0  21106  lgsqrlem5  21112  lgsquad  21124  dirith  21206  pntrmax  21241  qrngdiv  21301  padicabv  21307  pthistrl  21555  isspthonpth  21567  1pthon  21574  grpoasscan2  21809  grpoinvop  21812  grpopncan  21822  grponpcan  21823  grpopnpcan2  21824  gxneg  21837  gxneg2  21838  gxcom  21840  gxinv  21841  gxsuc  21843  gxadd  21846  gxnn0mul  21848  gxmul  21849  gxmodid  21850  rngoass  21958  rngosn  21975  zerdivemp1  22005  nvpncan2  22120  nvaddsub4  22125  nvnncan  22127  nvdif  22137  nvpi  22138  nvz  22141  nvabs  22145  nv1  22148  imsmetlem  22165  4ipval2  22187  lnoadd  22242  isblo3i  22285  hvsubass  22529  shlub  22899  homco2  23463  leopmul2i  23621  mdslmd4i  23819  atexch  23867  atcvatlem  23871  cdj3lem2  23921  cdj3lem2a  23922  iundisj2f  24013  curry2ima  24080  supxrnemnf  24110  snunioc  24120  ubico  24121  iundisj2fi  24136  divnumden2  24144  xreceu  24151  xdivcl  24153  xdivrec  24156  xrge0addass  24194  ofldaddlt  24224  rhmdvd  24242  redvr  24260  cnre2csqlem  24291  relogbcl  24385  logb1  24386  logblt  24389  hasheuni  24458  sigaclcuni  24484  difelsiga  24499  elsigagen2  24514  sigagenss2  24516  measbase  24534  measval  24535  ismeas  24536  isrnmeas  24537  measxun2  24547  measun  24548  measvunilem  24549  measvuni  24551  mbfmco2  24598  dya2iocnrect  24614  probun  24660  probdif  24661  totprob  24668  probmeasb  24671  cndprobin  24675  cndprobnul  24678  ballotlemfrcn0  24770  erdszelem2  24861  cvmcov2  24945  dedekindle  25171  mulcan1g  25172  subdivcomb1  25178  dfon2lem2  25390  frrlem3  25533  brbtwn  25781  brbtwn2  25787  colinearalglem1  25788  colinearalglem2  25789  colinearalg  25792  axcgrid  25798  ax5seglem1  25810  ax5seglem2  25811  axpasch  25823  axlowdimlem16  25839  axcontlem4  25849  axcontlem7  25852  cgrrflx  25864  cgrcomim  25866  cgrtr  25869  cgrtr3  25871  cgrcoml  25873  cgrcomr  25874  cgrtriv  25879  cgrdegen  25881  cgrextend  25885  segconeq  25887  segconeu  25888  btwntriv2  25889  btwntriv1  25893  btwnintr  25896  btwnexch3  25897  btwnouttr2  25899  btwnouttr  25901  btwnexch  25902  funtransport  25908  btwnxfr  25933  colinearex  25937  colineartriv1  25944  colineartriv2  25945  colinearxfr  25952  lineext  25953  linecgr  25958  lineid  25960  idinside  25961  btwnconn1lem7  25970  btwnconn1lem8  25971  btwnconn1lem9  25972  btwnconn1lem12  25975  btwnconn1lem14  25977  btwnconn3  25980  midofsegid  25981  segcon2  25982  seglerflx  25989  segletr  25991  outsidene1  26000  btwnoutside  26002  broutsideof3  26003  outsideoftr  26006  outsideofeq  26007  funray  26017  liness  26022  lineunray  26024  lineelsb2  26025  linecom  26027  linethru  26030  hilbert1.1  26031  bpolycl  26041  bpolydif  26044  areacirclem4  26225  areacirclem6  26228  areacirc  26229  elicc3  26252  clsun  26263  neiin  26267  finlocfin  26311  blbnd  26428  zerdivemp1x  26503  smprngopr  26594  isfldidl  26610  istopclsd  26686  ismrc  26687  mapco2g  26701  mapfzcons  26704  ofmpteq  26708  mzpcl34  26720  mzpexpmpt  26734  mzpsubst  26737  mzpresrename  26739  eldioph  26748  diophrw  26749  eqrabdioph  26768  lerabdioph  26797  ltrabdioph  26800  dvdsrabdioph  26802  diophren  26806  pellex  26830  pell14qrexpclnn0  26861  pellfundex  26881  rmxyadd  26916  rmyabs  26955  jm2.17a  26957  mzpcong  26969  acongeq  26980  coprmdvdsb  26984  modabsdifz  26988  jm2.22  26998  jm2.20nn  27000  rmxdiophlem  27018  rmxdioph  27019  jm3.1  27023  expdiophlem2  27025  islssfgi  27080  pwssplit0  27097  pwssplit1  27098  pwssplit2  27099  pwssplit3  27100  pwssplit4  27101  uvcresum  27152  frlmsplit2  27153  frlmsslss  27154  frlmup4  27163  islindf2  27194  lindsind2  27199  lindff1  27200  f1lindf  27202  lindsss  27204  f1linds  27205  cnsrexpcl  27280  pmtrfrn  27310  idomrootle  27421  fiuneneq  27423  ofdivrec  27453  ofdivcan4  27454  ubelsupr  27600  fnchoice  27609  fmul01  27619  fmuldfeq  27622  fmul01lt1lem2  27624  infrglb  27631  climsuse  27643  stoweidlem16  27674  stoweidlem20  27678  stoweidlem60  27718  wallispilem3  27725  sigaraf  27752  sigarmf  27753  sigaras  27754  sigarms  27755  sigarls  27756  sigarperm  27759  otiunsndisj  27996  otiunsndisjX  27997  leaddsuble  28012  nbfiusgrafi  28076  frg2woteu  28200  3orbi123  28347  alrim3con13v  28370  tratrb  28373  3orbi123VD  28714  19.21a3con13vVD  28716  tratrbVD  28725  bnj900  29052  bnj1110  29103  bnj1128  29111  bnj1125  29113  bnj1136  29118  bnj1189  29130  bnj1204  29133  bnj1321  29148  bnj1413  29156  lubunNEW  29502  lfladd  29595  lflsub  29596  lflmul  29597  lkrlsp2  29632  lshpkrlem5  29643  oplecon3b  29729  latm4  29762  omllaw4  29775  omllaw5N  29776  cmtcomlemN  29777  cmtbr2N  29782  cmtbr3N  29783  omlmod1i2N  29789  omlspjN  29790  cvrnbtwn3  29805  cvrcon3b  29806  cvrcmp  29812  cvrcmp2  29813  cvlatexch3  29867  cvlsupr5  29875  cvlsupr7  29877  hlrelat2  29931  2llnneN  29937  cvrval5  29943  cvrexch  29948  cvratlem  29949  atcvr0eq  29954  atcvrneN  29958  atcvrj1  29959  atle  29964  atlt  29965  atlelt  29966  2atjm  29973  3noncolr2  29977  3noncolr1N  29978  hlatcon2  29980  3dim1  29995  3dim2  29996  1cvratex  30001  1cvrat  30004  ps-1  30005  ps-2  30006  2atjlej  30007  hlatexch3N  30008  llnexatN  30049  llncmp  30050  lplni2  30065  lplnnle2at  30069  lplnnleat  30070  lplnri3N  30083  2lplnmN  30087  2llnmj  30088  lplncmp  30090  lplnexatN  30091  2llnm2N  30096  2llnm3N  30097  2llnmeqat  30099  2atnelvolN  30115  4atlem0ae  30122  4atlem0be  30123  4atlem3b  30126  4atlem9  30131  4atlem10a  30132  4atlem10  30134  lvolcmp  30145  2lplnm2N  30149  2lplnmj  30150  pmapglbx  30297  pmapmeet  30301  2llnma1b  30314  2llnma1  30315  2llnma3r  30316  2llnma2  30317  2llnma2rN  30318  elpadd2at  30334  paddasslem16  30363  padd4N  30368  paddclN  30370  pmodlem2  30375  pmapjoin  30380  pmapjat1  30381  pmapjat2  30382  hlmod1i  30384  atmod2i1  30389  atmod2i2  30390  atmod3i1  30392  llnexchb2  30397  dalawlem2  30400  elpcliN  30421  pclssN  30422  pclunN  30426  pclun2N  30427  polcon3N  30445  2polcon4bN  30446  paddunN  30455  poldmj1N  30456  pmapj2N  30457  pmapocjN  30458  psubclinN  30476  paddatclN  30477  poml5N  30482  osumcllem3N  30486  pexmidlem3N  30500  pexmidlem4N  30501  lhple  30570  lhpat4N  30572  4atex2  30605  4atex2-0bOLDN  30607  4atex3  30609  ltrnatb  30665  ltrnel  30667  ltrncnvel  30670  ltrncoelN  30671  ltrncoat  30672  ltrncoval  30673  ltrncnv  30674  ltrn11at  30675  ltrnmw  30679  trlcnv  30693  trljat2  30695  trlat  30697  trl0  30698  ltrnnidn  30702  trlnid  30707  trlval3  30715  trlval4  30716  cdlemc2  30720  cdlemc5  30723  cdlemc6  30724  cdlemd7  30732  cdleme00a  30737  cdleme0e  30745  cdleme01N  30749  cdleme02N  30750  cdleme0ex1N  30751  cdleme0ex2N  30752  cdleme3g  30762  cdleme3h  30763  cdleme3  30765  cdleme4  30766  cdleme5  30768  cdleme7b  30772  cdleme9  30781  cdleme11a  30788  cdleme11dN  30790  cdleme11e  30791  cdleme11g  30793  cdleme11h  30794  cdleme11j  30795  cdleme11k  30796  cdleme12  30799  cdleme18a  30819  cdleme18b  30820  cdleme18c  30821  cdleme22gb  30822  cdleme20zN  30829  cdleme20y  30830  cdleme19a  30831  cdleme20d  30840  cdleme20i  30845  cdleme20j  30846  cdleme20l2  30849  cdleme22a  30868  cdleme22d  30871  cdleme22e  30872  cdleme30a  30906  cdlemefs32sn1aw  30942  cdlemefs29bpre0N  30944  cdlemefs29bpre1N  30945  cdlemefs29cpre1N  30946  cdlemefs29clN  30947  cdleme43fsv1snlem  30948  cdlemefs32fvaN  30950  cdlemefs32fva1  30951  cdlemefs31fv1  30952  cdlemefs45eN  30959  cdleme41sn3a  30961  cdleme32fva  30965  cdleme32fvaw  30967  cdleme32b  30970  cdleme32c  30971  cdleme32e  30973  cdleme35h  30984  cdleme37m  30990  cdleme38m  30991  cdleme40m  30995  cdleme40n  30996  cdleme41sn3aw  31002  cdleme41sn4aw  31003  cdleme41fva11  31005  cdleme42b  31006  cdleme42e  31007  cdleme42h  31010  cdleme42i  31011  cdleme42k  31012  cdleme43cN  31019  cdleme17d2  31023  cdleme17d3  31024  cdleme48fv  31027  cdleme48bw  31030  cdleme48b  31031  cdlemeg47rv2  31038  cdlemeg46c  31041  cdlemeg46sfg  31048  cdlemeg46fjgN  31049  cdlemeg46rjgN  31050  cdlemeg46fjv  31051  cdlemeg46frv  31053  cdlemeg46vrg  31055  cdlemeg46rgv  31056  cdlemeg46req  31057  cdlemeg46gfv  31058  cdlemeg46gfre  31060  cdleme48d  31063  cdlemeg49lebilem  31067  cdleme50trn2  31079  cdleme50ltrn  31085  ltrniotacnvval  31110  ltrniotavalbN  31112  cdlemg1cex  31116  cdlemg2dN  31118  cdlemg2fvlem  31122  cdlemg2fv2  31128  cdlemg2kq  31130  cdlemg2l  31131  cdlemg2m  31132  cdlemg4a  31136  cdlemg4b1  31137  cdlemg4b2  31138  cdlemg4d  31141  cdlemg4e  31142  cdlemg4f  31143  cdlemg4  31145  cdlemg6d  31149  cdlemg6e  31150  cdlemg7fvN  31152  cdlemg8a  31155  cdlemg8b  31156  cdlemg8c  31157  cdlemg9a  31160  cdlemg9b  31161  cdlemg9  31162  cdlemg11aq  31166  cdlemg10c  31167  cdlemg12a  31171  cdlemg12b  31172  cdlemg12c  31173  cdlemg12f  31176  cdlemg12g  31177  cdlemg14f  31181  cdlemg14g  31182  cdlemg17a  31189  cdlemg17dN  31191  cdlemg17e  31193  cdlemg17i  31197  cdlemg17ir  31198  cdlemg17  31205  cdlemg18b  31207  cdlemg18c  31208  cdlemg18d  31209  cdlemg18  31210  cdlemg21  31214  cdlemg28a  31221  cdlemg31b0a  31223  cdlemg31a  31225  cdlemg31b  31226  cdlemg28b  31231  cdlemg33c  31236  cdlemg33d  31237  cdlemg33e  31238  cdlemg35  31241  cdlemg41  31246  ltrnco  31247  trlcocnv  31248  trlcoabs  31249  trlcoabs2N  31250  trlcocnvat  31252  trlconid  31253  trlcolem  31254  trlcone  31256  cdlemg42  31257  cdlemg43  31258  cdlemg44a  31259  cdlemg47a  31262  cdlemg46  31263  trljco  31268  tendoset  31287  tendof  31291  tendoeq1  31292  tendocoval  31294  tendoco2  31296  tendococl  31300  tendoplcl2  31306  tendoplco2  31307  tendopltp  31308  tendoplcl  31309  tendoplcom  31310  cdlemh  31345  cdlemi1  31346  cdlemi2  31347  cdlemk1  31359  cdlemk2  31360  cdlemk3  31361  cdlemk4  31362  cdlemk8  31366  cdlemk9  31367  cdlemk9bN  31368  cdlemki  31369  cdlemkvcl  31370  cdlemk10  31371  cdlemksv2  31375  cdlemk7  31376  cdlemk11  31377  cdlemk12  31378  cdlemk5u  31389  cdlemk6u  31390  cdlemk7u  31398  cdlemk12u  31400  cdlemk22  31421  cdlemk32  31425  cdlemk28-3  31436  cdlemk34  31438  cdlemk29-3  31439  cdlemk39  31444  cdlemkfid1N  31449  cdlemkid1  31450  cdlemkid2  31452  cdlemkfid3N  31453  cdlemk54  31486  cdlemk19u  31498  cdlemk56w  31501  tendoex  31503  cdleml1N  31504  cdleml2N  31505  cdleml3N  31506  cdleml6  31509  cdleml7  31510  cdleml8  31511  cdleml9  31512  tendocnv  31550  tendospcanN  31552  dvhopvadd  31622  tendolinv  31634  tendorinv  31635  dicvaddcl  31719  dicvscacl  31720  cdlemn2  31724  cdlemn2a  31725  cdlemn3  31726  cdlemn4  31727  cdlemn4a  31728  cdlemn5pre  31729  cdlemn6  31731  cdlemn7  31732  cdlemn8  31733  cdlemn9  31734  cdlemn10  31735  cdlemn11a  31736  cdlemn11c  31738  cdlemn11pre  31739  dihordlem6  31742  dihordlem7  31743  dihordlem7b  31744  dihjustlem  31745  dihjust  31746  dihord2cN  31750  dihord11c  31753  dihvalcq2  31776  dihopelvalcpre  31777  dihmeetlem1N  31819  dihglblem3N  31824  dihmeetlem2N  31828  dihglbcpreN  31829  dihmeetcN  31831  dihmeetbclemN  31833  dihmeetlem4preN  31835  dihmeetlem9N  31844  dihmeetlem13N  31848  dihmeetlem20N  31855  dih1dimatlem0  31857  dihlspsnat  31862  dihmeet  31872  dochss  31894  dochdmj1  31919  hdmap1fval  32326  hdmapfval  32359  hgmapfval  32418
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