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

Theorem simp1 955
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 952 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simpld 445 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  simpl1  958  simpr1  961  simp1i  964  simp1d  967  simp11  985  simp21  988  simp31  991  syld3an3  1227  rsp2e  2607  fresaun  5378  foco2  5642  fsnunf  5680  fsnunf2  5681  fnsuppres  5694  fcofo  5760  fveqf1o  5768  f1oiso2  5811  ovmpt2x  5938  ovmpt2ga  5939  ofeq  6042  ofrval  6050  riotass  6329  riotasv2s  6347  onoviun  6356  omwordri  6566  omeulem1  6576  oeord  6582  oewordri  6586  oeordsuc  6588  erov  6751  mapxpen  7023  unbnn  7109  fofinf1o  7133  elfir  7165  dffi2  7172  elfiun  7179  fisup2g  7213  suppr  7215  ordtype2  7245  hartogslem1  7253  wemapso  7262  wemapso2  7263  ixpiunwdom  7301  cnfcom3clem  7404  cdaassen  7804  mapcdaen  7806  infcdaabs  7828  infunabs  7829  infdif  7831  infdif2  7832  cfsmolem  7892  isf32lem11  7985  isf34lem7  8001  zornn0g  8128  ttukey2g  8139  konigthlem  8186  gchdomtri  8247  fpwwe  8264  canthwe  8269  gchaleph  8293  gchaleph2  8294  winainflem  8311  wununi  8324  tsksuc  8380  tskpr  8388  tskop  8389  tskcard  8399  grupw  8413  grurn  8419  gruop  8423  gruun  8424  grumap  8426  gruixp  8427  distrlem4pr  8646  ltadd2  8920  mul31  8976  readdcan  8982  addid2  8991  addsubass  9057  subcan2  9068  subsub2  9071  subsub4  9076  npncan3  9081  pnpcan  9082  pnncan  9084  subcan  9098  subdi  9209  ltadd1  9237  leadd1  9238  leadd2  9239  ltsubadd  9240  lesubadd  9242  lesub1  9264  lesub2  9265  ltsub1  9266  ltsub2  9267  mulcan  9401  mulcan2  9402  divcan2  9428  diveq0  9430  divrec  9436  divrec2  9437  divdir  9443  divcan3  9444  div11  9446  divcan5  9458  redivcl  9475  div2neg  9479  ltmul1  9602  ltdiv1  9616  ltmuldiv  9622  ledivmulOLD  9626  lemuldiv  9631  lt2msq1  9635  suprub  9711  suprlub  9712  infmsup  9728  infmrgelb  9730  infmrlb  9731  ofsubeq0  9739  ofnegsub  9740  ofsubge0  9741  gtndiv  10085  eluz2  10232  peano2uz  10268  suprzub  10305  xrltmin  10507  xrlemin  10509  xaddass  10565  xleadd1  10571  xltadd1  10572  xmulass  10603  xlemul1  10606  xlemul2  10607  xltmul1  10608  xadddi  10611  xadddir  10612  xadddi2  10613  supxrre  10642  infmxrre  10650  ixxssixx  10666  ixxub  10673  ixxlb  10674  lbico1  10702  lbicc2  10748  icoshftf1o  10755  snunioo  10758  snunico  10759  iccsplit  10764  fzrev3  10845  fzm1  10858  fzrevral2  10863  elfzo0  10900  flwordi  10938  flword2  10939  expgt1  11136  exprec  11139  leexp2a  11153  expubnd  11158  sqdiv  11165  expnbnd  11226  expmulnbnd  11229  modexp  11232  bccmpl  11318  ccatass  11432  swrdval  11446  swrdval2  11449  ccatco  11486  s3cl  11523  swrds2  11556  mulre  11602  caubnd  11838  climuni  12022  iseraltlem3  12152  geoisum1c  12332  eflt  12393  rpnnen2lem4  12492  dvdsmultr2  12560  dvdsexp  12580  sadass  12658  dvdsgcdb  12719  gcdass  12720  mulgcd  12721  gcddiv  12724  rplpwr  12731  coprmdvds  12777  mulgcddvds  12779  qredeq  12781  rpexp12i  12797  rpmul  12798  odzcllem  12853  odzphi  12857  pythagtriplem15  12878  pcpremul  12892  pcdiv  12901  pcqmul  12902  pcqdiv  12906  vdwapfval  13014  vdwapun  13017  vdwpc  13023  hashbcss  13047  ramval  13051  0ram2  13064  0ramcl  13066  ramcl  13072  ressbas  13194  xpsadd  13474  xpsmul  13475  mreiincl  13494  mreincl  13497  mrcss  13514  mrcun  13520  submrc  13526  posasymb  14082  meetle  14130  p0le  14145  ple1  14146  latleeqj1  14165  latjlej12  14169  latleeqm1  14181  latmlem12  14185  latnlemlt  14186  latj4  14203  latj4rot  14204  lubss  14221  lubun  14223  clatglbss  14227  pospropd  14234  isipodrs  14260  imasmnd2  14405  gsumccat  14460  frmdup3  14484  grpinvadd  14540  grpsubeq0  14548  grppncan  14552  grpsubpropd2  14563  pwsinvg  14603  imasgrp2  14606  issubg  14617  nsgconj  14646  nsgid  14659  ghmnsgima  14702  odcong  14860  isslw  14915  pgpssslw  14921  lsmsubg  14961  efgsval2  15038  frgpup3  15083  cmn4  15104  ablinvadd  15107  ablsub4  15110  abladdsub4  15111  ablpncan2  15113  lsmsubg2  15147  lsm4  15148  rngcom  15365  imasrng  15398  unitmulcl  15442  unitmulclb  15443  dvrcan1  15469  dvrcan3  15470  irredrmul  15485  isabvd  15581  abvdom  15599  islmod  15627  lmodvsnegOLD  15664  lmodcom  15667  lss0cl  15700  lssvnegcl  15709  lssincl  15718  lspss  15737  lspun  15740  lspsnvsi  15757  lsslsp  15768  lmodvsinv  15789  lmodvsinv2  15790  0lmhm  15793  lsmsp  15835  lsmsp2  15836  lspvadd  15845  lspsntri  15846  lidldvgen  16003  rrgeq0  16027  aspid  16066  aspss  16068  asclmul1  16075  asclmul2  16076  psrbagaddcl  16112  psrbagconcl  16115  coe1tm  16345  coe1sclmul  16354  coe1sclmul2  16356  phllmhm  16532  ip2eq  16553  cssmre  16589  iuncld  16778  clsss  16787  ntrin  16794  clsndisj  16808  iscldtop  16828  neiss  16842  lpss3  16872  restco  16891  restabs  16892  restcldi  16900  restcls  16907  restntr  16908  restlp  16909  lmconst  16987  cnpresti  17012  hausnei2  17077  sshauslem  17096  clscon  17152  concompss  17155  concompclo  17157  kgen2ss  17246  elptr  17264  xkococn  17350  qtopval2  17383  qtoptop2  17386  cmphaushmeo  17487  elmptrab  17518  filinn0  17551  fbasweak  17556  snfbas  17557  filuni  17576  trnei  17583  fmval  17634  rnelfm  17644  flimrest  17674  flimclslem  17675  flfnei  17682  isflf  17684  lmflf  17696  fclsneii  17708  fclsrest  17715  isfcf  17725  ptcmpg  17747  istgp2  17770  divstgpopn  17798  divstgphaus  17801  xmetge0  17905  xmetsym  17908  xmetresbl  17979  mopni3  18036  stdbdxmet  18057  stdbdmopn  18060  prdsxms  18072  prdsms  18073  isngp4  18129  nmsub  18140  nm2dif  18142  nminvr  18176  nmoix  18234  nmods  18249  metds0  18350  metnrm  18362  cncfmptc  18411  iirev  18423  icoopnst  18433  iocopnst  18434  icchmeo  18435  iccpnfhmeo  18439  pi1blem  18533  pi1xfr  18549  isclmi  18571  cphsqrcl  18616  cph2ass  18644  ipcau  18664  nmpar  18666  fmcfil  18694  iscau3  18700  cmetcaulem  18710  cfilres  18718  bcthlem1  18742  bcthlem5  18746  cncdrg  18772  rlmbn  18774  cniccbdd  18817  ovolunnul  18855  ovolicc  18878  iundisj2  18902  ovolioo  18921  volcn  18957  itg1le  19064  itg2le  19090  iblcnlem  19139  dvfval  19243  dvid  19263  dvcnp2  19265  dvnf  19272  dvnbss  19273  dvn2bss  19275  evlsval2  19400  tdeglem3  19441  mdegldg  19448  mdegmullem  19460  deg1ldgdomn  19476  deg1lt  19479  deg1scl  19495  deg1mul3  19497  q1peqb  19536  fta1b  19551  elplyr  19579  ply1term  19582  dgrub  19612  coe1term  19636  dgradd2  19645  dgrmulc  19648  ofmulrt  19658  quotcl2  19678  quotdgr  19679  facth  19682  quotcan  19685  aannenlem1  19704  aannenlem2  19705  ulmf  19757  ptolemy  19860  tanord1  19895  efif1o  19904  argrege0  19961  logimul  19964  cxpneg  20024  ang180lem1  20103  ang180lem2  20104  ang180lem3  20105  ang180lem4  20106  isosctrlem2  20115  cxp2lim  20267  amgmlem  20280  wilthlem3  20304  sgmppw  20432  lgslem1  20531  lgsneg  20554  lgssq2  20571  lgsdirnn0  20574  lgsqrlem5  20580  lgsquad  20592  dirith  20674  pntrmax  20709  qrngdiv  20769  padicabv  20775  grpoasscan2  20899  grpoinvop  20902  grpopncan  20912  grponpcan  20913  grpopnpcan2  20914  gxneg  20927  gxneg2  20928  gxcom  20930  gxinv  20931  gxsuc  20933  gxadd  20936  gxnn0mul  20938  gxmul  20939  gxmodid  20940  rngoass  21048  rngosn  21065  nvpncan2  21208  nvaddsub4  21213  nvnncan  21215  nvdif  21225  nvpi  21226  nvz  21229  nvabs  21233  nv1  21236  imsmetlem  21253  4ipval2  21275  lnoadd  21330  isblo3i  21373  hvsubass  21619  shlub  21989  homco2  22553  leopmul2i  22711  mdslmd4i  22909  atexch  22957  atcvatlem  22961  cdj3lem2  23011  cdj3lem2a  23012  ballotlemsgt1  23065  ballotlemfrcn0  23084  erdszelem2  23130  cvmcov2  23213  dedekindle  23489  mulcan1g  23490  subdivcomb1  23496  dfon2lem2  23544  frrlem3  23687  axfelem17  23766  brbtwn  23937  brbtwn2  23943  colinearalglem1  23944  colinearalglem2  23945  colinearalg  23948  axcgrid  23954  ax5seglem1  23966  ax5seglem2  23967  axpasch  23979  axlowdimlem16  23995  axcontlem4  24005  axcontlem7  24008  cgrrflx  24020  cgrcomim  24022  cgrtr  24025  cgrtr3  24027  cgrcoml  24029  cgrcomr  24030  cgrtriv  24035  cgrdegen  24037  cgrextend  24041  segconeq  24043  segconeu  24044  btwntriv2  24045  btwntriv1  24049  btwnintr  24052  btwnexch3  24053  btwnouttr2  24055  btwnouttr  24057  btwnexch  24058  funtransport  24064  btwnxfr  24089  colinearex  24093  colineartriv1  24100  colineartriv2  24101  colinearxfr  24108  lineext  24109  linecgr  24114  lineid  24116  idinside  24117  btwnconn1lem7  24126  btwnconn1lem8  24127  btwnconn1lem9  24128  btwnconn1lem12  24131  btwnconn1lem14  24133  btwnconn3  24136  midofsegid  24137  segcon2  24138  seglerflx  24145  segletr  24147  outsidene1  24156  btwnoutside  24158  broutsideof3  24159  outsideoftr  24162  outsideofeq  24163  funray  24173  liness  24178  lineunray  24180  lineelsb2  24181  linecom  24183  linethru  24186  hilbert1.1  24187  bpolycl  24197  bpolydif  24200  areacirclem4  24337  areacirc  24341  intn3an1d  24346  infxpg  24505  ab2rexex2g  24543  iccleub3  24547  injsurinj  24560  iscst1  24585  jop  24595  cur1vald  24610  preotr2  24646  prltub  24671  ubpar  24672  inposet  24689  dfps2  24700  reacomsmgrp1  24754  reacomsmgrp3  24756  reacomsmgrp4  24757  clfsebs  24758  clfsebsr  24760  fprodadd  24763  abloinvop  24764  mndoio  24769  fprodneg  24789  fprodsub  24790  prsubrtr  24810  multinv  24833  multinvb  24834  fldax3  24841  zerdivemp1  24847  mulveczer  24890  mulinvsca  24891  glmrngo  24893  truni1  24916  npmp  24932  mapdiscn  24938  hmeogrpi  24947  conttnf2  24973  bwt2  25003  mslb1  25018  msra3  25020  limnumrr  25033  lvsovso2  25038  claddrvr  25059  issubrv  25083  ismulcv  25092  clsmulrv  25094  mulmulvec  25098  distmlva  25099  distsava  25100  isdivcv2  25104  divclcvd  25105  divclrvd  25106  imonclem  25224  ismonc  25225  cmpmon  25226  icmpmon  25227  isepic  25235  tartarmap  25299  rocatval  25370  cmp2morpcats  25372  cmp2morpgrp  25374  cmp2morpdom  25375  cmp2morpcod  25376  cmpmorass  25377  indcls2  25407  bisig0  25473  isconcl6a  25514  isib2g1a1  25527  isibg2a1  25530  segline  25552  pxysxy  25553  isibcg  25602  elicc3  25639  clsun  25657  neiin  25661  finlocfin  25710  blbnd  25922  zerdivemp1x  25997  smprngopr  26088  isfldidl  26104  istopclsd  26186  ismrc  26187  mapco2g  26201  mapfzcons  26204  ofmpteq  26208  mzpcl34  26220  mzpexpmpt  26234  mzpsubst  26237  mzpresrename  26239  eldioph  26248  diophrw  26249  eqrabdioph  26268  lerabdioph  26297  ltrabdioph  26300  dvdsrabdioph  26302  diophren  26307  pellex  26331  pell14qrexpclnn0  26362  pellfundex  26382  rmxyadd  26417  rmyabs  26456  jm2.17a  26458  mzpcong  26470  acongeq  26481  coprmdvdsb  26485  modabsdifz  26489  jm2.22  26499  jm2.20nn  26501  rmxdiophlem  26519  rmxdioph  26520  jm3.1  26524  expdiophlem2  26526  islssfgi  26581  pwssplit0  26598  pwssplit1  26599  pwssplit2  26600  pwssplit3  26601  pwssplit4  26602  uvcresum  26653  frlmsplit2  26654  frlmsslss  26655  frlmup4  26664  islindf2  26695  lindsind2  26700  lindff1  26701  f1lindf  26703  lindsss  26705  f1linds  26706  cnsrexpcl  26781  pmtrfrn  26811  idomrootle  26922  fiuneneq  26924  ofdivrec  26954  ofdivcan4  26955  ubelsupr  27102  fnchoice  27111  fmul01  27121  fmuldfeq  27124  fmul01lt1lem2  27126  infrglb  27133  climsuse  27145  ibliccsinexp  27156  stoweidlem16  27176  stoweidlem20  27180  stoweidlem22  27182  stoweidlem26  27186  stoweidlem31  27191  stoweidlem34  27194  stoweidlem43  27203  stoweidlem44  27204  stoweidlem51  27211  stoweidlem52  27212  stoweidlem57  27217  stoweidlem60  27220  wallispilem3  27227  3orbi123  27556  alrim3con13v  27579  tratrb  27582  3orbi123VD  27906  19.21a3con13vVD  27908  tratrbVD  27917  bnj900  28240  bnj1110  28291  bnj1128  28299  bnj1125  28301  bnj1136  28306  bnj1189  28318  bnj1204  28321  bnj1321  28336  bnj1413  28344  lubunNEW  28442  lfladd  28535  lflsub  28536  lflmul  28537  lkrlsp2  28572  lshpkrlem5  28583  oplecon3b  28669  latm4  28702  omllaw4  28715  omllaw5N  28716  cmtcomlemN  28717  cmtbr2N  28722  cmtbr3N  28723  omlmod1i2N  28729  omlspjN  28730  cvrnbtwn3  28745  cvrcon3b  28746  cvrcmp  28752  cvrcmp2  28753  cvlatexch3  28807  cvlsupr5  28815  cvlsupr7  28817  hlrelat2  28871  2llnneN  28877  cvrval5  28883  cvrexch  28888  cvratlem  28889  atcvr0eq  28894  atcvrneN  28898  atcvrj1  28899  atle  28904  atlt  28905  atlelt  28906  2atjm  28913  3noncolr2  28917  3noncolr1N  28918  hlatcon2  28920  3dim1  28935  3dim2  28936  1cvratex  28941  1cvrat  28944  ps-1  28945  ps-2  28946  2atjlej  28947  hlatexch3N  28948  llnexatN  28989  llncmp  28990  lplni2  29005  lplnnle2at  29009  lplnnleat  29010  lplnri3N  29023  2lplnmN  29027  2llnmj  29028  lplncmp  29030  lplnexatN  29031  2llnm2N  29036  2llnm3N  29037  2llnmeqat  29039  2atnelvolN  29055  4atlem0ae  29062  4atlem0be  29063  4atlem3b  29066  4atlem9  29071  4atlem10a  29072  4atlem10  29074  lvolcmp  29085  2lplnm2N  29089  2lplnmj  29090  pmapglbx  29237  pmapmeet  29241  2llnma1b  29254  2llnma1  29255  2llnma3r  29256  2llnma2  29257  2llnma2rN  29258  elpadd2at  29274  paddasslem16  29303  padd4N  29308  paddclN  29310  pmodlem2  29315  pmapjoin  29320  pmapjat1  29321  pmapjat2  29322  hlmod1i  29324  atmod2i1  29329  atmod2i2  29330  atmod3i1  29332  llnexchb2  29337  dalawlem2  29340  elpcliN  29361  pclssN  29362  pclunN  29366  pclun2N  29367  polcon3N  29385  2polcon4bN  29386  paddunN  29395  poldmj1N  29396  pmapj2N  29397  pmapocjN  29398  psubclinN  29416  paddatclN  29417  poml5N  29422  osumcllem3N  29426  pexmidlem3N  29440  pexmidlem4N  29441  lhple  29510  lhpat4N  29512  4atex2  29545  4atex2-0bOLDN  29547  4atex3  29549  ltrnatb  29605  ltrnel  29607  ltrncnvel  29610  ltrncoelN  29611  ltrncoat  29612  ltrncoval  29613  ltrncnv  29614  ltrn11at  29615  ltrnmw  29619  trlcnv  29633  trljat2  29635  trlat  29637  trl0  29638  ltrnnidn  29642  trlnid  29647  trlval3  29655  trlval4  29656  cdlemc2  29660  cdlemc5  29663  cdlemc6  29664  cdlemd7  29672  cdleme00a  29677  cdleme0e  29685  cdleme01N  29689  cdleme02N  29690  cdleme0ex1N  29691  cdleme0ex2N  29692  cdleme3g  29702  cdleme3h  29703  cdleme3  29705  cdleme4  29706  cdleme5  29708  cdleme7b  29712  cdleme9  29721  cdleme11a  29728  cdleme11dN  29730  cdleme11e  29731  cdleme11g  29733  cdleme11h  29734  cdleme11j  29735  cdleme11k  29736  cdleme12  29739  cdleme18a  29759  cdleme18b  29760  cdleme18c  29761  cdleme22gb  29762  cdleme20zN  29769  cdleme20y  29770  cdleme19a  29771  cdleme20d  29780  cdleme20i  29785  cdleme20j  29786  cdleme20l2  29789  cdleme22a  29808  cdleme22d  29811  cdleme22e  29812  cdleme30a  29846  cdlemefs32sn1aw  29882  cdlemefs29bpre0N  29884  cdlemefs29bpre1N  29885  cdlemefs29cpre1N  29886  cdlemefs29clN  29887  cdleme43fsv1snlem  29888  cdlemefs32fvaN  29890  cdlemefs32fva1  29891  cdlemefs31fv1  29892  cdlemefs45eN  29899  cdleme41sn3a  29901  cdleme32fva  29905  cdleme32fvaw  29907  cdleme32b  29910  cdleme32c  29911  cdleme32e  29913  cdleme35h  29924  cdleme37m  29930  cdleme38m  29931  cdleme40m  29935  cdleme40n  29936  cdleme41sn3aw  29942  cdleme41sn4aw  29943  cdleme41fva11  29945  cdleme42b  29946  cdleme42e  29947  cdleme42h  29950  cdleme42i  29951  cdleme42k  29952  cdleme43cN  29959  cdleme17d2  29963  cdleme17d3  29964  cdleme48fv  29967  cdleme48bw  29970  cdleme48b  29971  cdlemeg47rv2  29978  cdlemeg46c  29981  cdlemeg46sfg  29988  cdlemeg46fjgN  29989  cdlemeg46rjgN  29990  cdlemeg46fjv  29991  cdlemeg46frv  29993  cdlemeg46vrg  29995  cdlemeg46rgv  29996  cdlemeg46req  29997  cdlemeg46gfv  29998  cdlemeg46gfre  30000  cdleme48d  30003  cdlemeg49lebilem  30007  cdleme50trn2  30019  cdleme50ltrn  30025  ltrniotacnvval  30050  ltrniotavalbN  30052  cdlemg1cex  30056  cdlemg2dN  30058  cdlemg2fvlem  30062  cdlemg2fv2  30068  cdlemg2kq  30070  cdlemg2l  30071  cdlemg2m  30072  cdlemg4a  30076  cdlemg4b1  30077  cdlemg4b2  30078  cdlemg4d  30081  cdlemg4e  30082  cdlemg4f  30083  cdlemg4  30085  cdlemg6d  30089  cdlemg6e  30090  cdlemg7fvN  30092  cdlemg8a  30095  cdlemg8b  30096  cdlemg8c  30097  cdlemg9a  30100  cdlemg9b  30101  cdlemg9  30102  cdlemg11aq  30106  cdlemg10c  30107  cdlemg12a  30111  cdlemg12b  30112  cdlemg12c  30113  cdlemg12f  30116  cdlemg12g  30117  cdlemg14f  30121  cdlemg14g  30122  cdlemg17a  30129  cdlemg17dN  30131  cdlemg17e  30133  cdlemg17i  30137  cdlemg17ir  30138  cdlemg17  30145  cdlemg18b  30147  cdlemg18c  30148  cdlemg18d  30149  cdlemg18  30150  cdlemg21  30154  cdlemg28a  30161  cdlemg31b0a  30163  cdlemg31a  30165  cdlemg31b  30166  cdlemg28b  30171  cdlemg33c  30176  cdlemg33d  30177  cdlemg33e  30178  cdlemg35  30181  cdlemg41  30186  ltrnco  30187  trlcocnv  30188  trlcoabs  30189  trlcoabs2N  30190  trlcocnvat  30192  trlconid  30193  trlcolem  30194  trlcone  30196  cdlemg42  30197  cdlemg43  30198  cdlemg44a  30199  cdlemg47a  30202  cdlemg46  30203  trljco  30208  tendoset  30227  tendof  30231  tendoeq1  30232  tendocoval  30234  tendoco2  30236  tendococl  30240  tendoplcl2  30246  tendoplco2  30247  tendopltp  30248  tendoplcl  30249  tendoplcom  30250  cdlemh  30285  cdlemi1  30286  cdlemi2  30287  cdlemk1  30299  cdlemk2  30300  cdlemk3  30301  cdlemk4  30302  cdlemk8  30306  cdlemk9  30307  cdlemk9bN  30308  cdlemki  30309  cdlemkvcl  30310  cdlemk10  30311  cdlemksv2  30315  cdlemk7  30316  cdlemk11  30317  cdlemk12  30318  cdlemk5u  30329  cdlemk6u  30330  cdlemk7u  30338  cdlemk12u  30340  cdlemk22  30361  cdlemk32  30365  cdlemk28-3  30376  cdlemk34  30378  cdlemk29-3  30379  cdlemk39  30384  cdlemkfid1N  30389  cdlemkid1  30390  cdlemkid2  30392  cdlemkfid3N  30393  cdlemk54  30426  cdlemk19u  30438  cdlemk56w  30441  tendoex  30443  cdleml1N  30444  cdleml2N  30445  cdleml3N  30446  cdleml6  30449  cdleml7  30450  cdleml8  30451  cdleml9  30452  tendocnv  30490  tendospcanN  30492  dvhopvadd  30562  tendolinv  30574  tendorinv  30575  dicvaddcl  30659  dicvscacl  30660  cdlemn2  30664  cdlemn2a  30665  cdlemn3  30666  cdlemn4  30667  cdlemn4a  30668  cdlemn5pre  30669  cdlemn6  30671  cdlemn7  30672  cdlemn8  30673  cdlemn9  30674  cdlemn10  30675  cdlemn11a  30676  cdlemn11c  30678  cdlemn11pre  30679  dihordlem6  30682  dihordlem7  30683  dihordlem7b  30684  dihjustlem  30685  dihjust  30686  dihord2cN  30690  dihord11c  30693  dihvalcq2  30716  dihopelvalcpre  30717  dihmeetlem1N  30759  dihglblem3N  30764  dihmeetlem2N  30768  dihglbcpreN  30769  dihmeetcN  30771  dihmeetbclemN  30773  dihmeetlem4preN  30775  dihmeetlem9N  30784  dihmeetlem13N  30788  dihmeetlem20N  30795  dih1dimatlem0  30797  dihlspsnat  30802  dihmeet  30812  dochss  30834  dochdmj1  30859  hdmap1fval  31266  hdmapfval  31299  hgmapfval  31358
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator