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  2729  funtpg  5460  feq123  5543  fresaun  5573  foco2  5848  ftpg  5875  fsnunf  5890  fsnunf2  5891  fnsuppres  5911  fcofo  5980  fveqf1o  5988  f1oiso2  6031  ovmpt2x  6161  ovmpt2ga  6162  ofeq  6266  ofrval  6274  riotass  6537  riotasv2s  6555  onoviun  6564  omwordri  6774  omeulem1  6784  oeord  6790  oewordri  6794  oeordsuc  6796  erov  6960  mapxpen  7232  unbnn  7322  fofinf1o  7346  elfir  7378  inelfi  7381  dffi2  7386  elfiun  7393  fisup2g  7427  suppr  7429  ordtype2  7459  hartogslem1  7467  wemapso  7476  wemapso2  7477  ixpiunwdom  7515  cnfcom3clem  7618  cdaassen  8018  mapcdaen  8020  infcdaabs  8042  infunabs  8043  infdif  8045  infdif2  8046  cfsmolem  8106  isf32lem11  8199  isf34lem7  8215  zornn0g  8341  ttukey2g  8352  konigthlem  8399  gchdomtri  8460  fpwwe  8477  canthwe  8482  gchaleph  8506  gchaleph2  8507  winainflem  8524  wununi  8537  tsksuc  8593  tskpr  8601  tskop  8602  tskcard  8612  grupw  8626  grurn  8632  gruop  8636  gruun  8637  grumap  8639  gruixp  8640  distrlem4pr  8859  ltadd2  9133  mul31  9190  readdcan  9196  addid2  9205  addsubass  9271  subcan2  9282  subsub2  9285  subsub4  9290  npncan3  9295  pnpcan  9296  pnncan  9298  subcan  9312  subdi  9423  ltadd1  9451  leadd1  9452  leadd2  9453  ltsubadd  9454  lesubadd  9456  lesub1  9478  lesub2  9479  ltsub1  9480  ltsub2  9481  mulcan  9615  mulcan2  9616  divcan2  9642  diveq0  9644  divrec  9650  divrec2  9651  divdir  9657  divcan3  9658  div11  9660  divcan5  9672  redivcl  9689  div2neg  9693  ltmul1  9816  ltdiv1  9830  ltmuldiv  9836  ledivmulOLD  9840  lemuldiv  9845  lt2msq1  9849  suprub  9925  suprlub  9926  infmsup  9942  infmrgelb  9944  infmrlb  9945  ofsubeq0  9953  ofnegsub  9954  ofsubge0  9955  gtndiv  10303  eluz2  10450  peano2uz  10486  suprzub  10523  xrltmin  10726  xrlemin  10728  xaddass  10784  xleadd1  10790  xltadd1  10791  xmulass  10822  xlemul1  10825  xlemul2  10826  xltmul1  10827  xadddi  10830  xadddir  10831  xadddi2  10832  supxrre  10862  infmxrre  10870  ixxssixx  10886  ixxub  10893  ixxlb  10894  lbico1  10922  lbicc2  10969  icoshftf1o  10976  snunioo  10979  snunico  10980  iccsplit  10985  fzrev3  11067  fzm1  11082  fzrevral2  11087  elfzo0  11126  flwordi  11174  flword2  11175  expgt1  11373  exprec  11376  leexp2a  11390  expubnd  11395  sqdiv  11402  expnbnd  11463  expmulnbnd  11466  modexp  11469  bccmpl  11555  ccatass  11705  swrdval  11719  swrdval2  11722  ccatco  11759  s3cl  11796  swrds2  11835  mulre  11881  caubnd  12117  climuni  12301  iseraltlem3  12432  geoisum1c  12612  eflt  12673  rpnnen2lem4  12772  dvdsmultr2  12840  dvdsexp  12860  sadass  12938  dvdsgcdb  12999  gcdass  13000  mulgcd  13001  gcddiv  13004  rplpwr  13011  coprmdvds  13057  mulgcddvds  13059  qredeq  13061  rpexp12i  13077  rpmul  13078  odzcllem  13133  odzphi  13137  pythagtriplem15  13158  pcpremul  13172  pcdiv  13181  pcqmul  13182  pcqdiv  13186  vdwapfval  13294  vdwapun  13297  vdwpc  13303  hashbcss  13327  ramval  13331  0ram2  13344  0ramcl  13346  ramcl  13352  ressbas  13474  xpsadd  13756  xpsmul  13757  mreiincl  13776  mreincl  13779  mrcss  13796  mrcun  13802  submrc  13808  posasymb  14364  meetle  14412  p0le  14427  ple1  14428  latleeqj1  14447  latjlej12  14451  latleeqm1  14463  latmlem12  14467  latnlemlt  14468  latj4  14485  latj4rot  14486  lubss  14503  lubun  14505  clatglbss  14509  pospropd  14516  isipodrs  14542  imasmnd2  14687  gsumccat  14742  frmdup3  14766  grpinvadd  14822  grpsubeq0  14830  grppncan  14834  grpsubpropd2  14845  pwsinvg  14885  imasgrp2  14888  issubg  14899  nsgconj  14928  nsgid  14941  ghmnsgima  14984  odcong  15142  isslw  15197  pgpssslw  15203  lsmsubg  15243  efgsval2  15320  frgpup3  15365  cmn4  15386  ablinvadd  15389  ablsub4  15392  abladdsub4  15393  ablpncan2  15395  lsmsubg2  15429  lsm4  15430  rngcom  15647  imasrng  15680  unitmulcl  15724  unitmulclb  15725  dvrcan1  15751  dvrcan3  15752  irredrmul  15767  isabvd  15863  abvdom  15881  islmod  15909  lmodcom  15945  lss0cl  15978  lssvnegcl  15987  lssincl  15996  lspss  16015  lspun  16018  lspsnvsi  16035  lsslsp  16046  lmodvsinv  16067  lmodvsinv2  16068  0lmhm  16071  lsmsp  16113  lsmsp2  16114  lspvadd  16123  lspsntri  16124  lidldvgen  16281  rrgeq0  16305  aspid  16344  aspss  16346  asclmul1  16353  asclmul2  16354  psrbagaddcl  16390  psrbagconcl  16393  coe1tm  16620  coe1sclmul  16629  coe1sclmul2  16631  phllmhm  16818  ip2eq  16839  cssmre  16875  iuncld  17064  clsss  17073  ntrin  17080  clsndisj  17094  iscldtop  17114  neiss  17128  lpss3  17163  restco  17182  restabs  17183  restcldi  17191  neitr  17198  restcls  17199  restntr  17200  restlp  17201  lmconst  17279  cnpresti  17306  hausnei2  17371  sshauslem  17390  clscon  17446  concompss  17449  concompclo  17451  kgen2ss  17540  elptr  17558  xkococn  17645  qtopval2  17681  qtoptop2  17684  cmphaushmeo  17785  elmptrab  17812  filinn0  17845  fbasweak  17850  snfbas  17851  filuni  17870  trnei  17877  fmval  17928  rnelfm  17938  flimrest  17968  flimclslem  17969  flfnei  17976  isflf  17978  lmflf  17990  fclsneii  18002  fclsrest  18009  isfcf  18019  ptcmpg  18041  istgp2  18074  divstgpopn  18102  divstgphaus  18105  ustfn  18184  ustval  18185  isust  18186  ustssel  18188  ustn0  18203  trust  18212  utop2nei  18233  ressusp  18248  trcfilu  18277  cfiluweak  18278  psmetsym  18294  psmetge0  18296  xmetge0  18327  xmetsym  18330  xmetresbl  18420  mopni3  18477  stdbdxmet  18498  stdbdmopn  18501  prdsxms  18513  prdsms  18514  metustblOLD  18563  metustbl  18564  xmsuspOLD  18568  xmsusp  18569  restmetu  18570  isngp4  18611  nmsub  18622  nm2dif  18624  nminvr  18658  nmoix  18716  nmods  18731  metds0  18833  metnrm  18845  cncfmptc  18894  iirev  18907  icoopnst  18917  iocopnst  18918  icchmeo  18919  iccpnfhmeo  18923  pi1blem  19017  isclmi  19055  cphsqrcl  19100  cph2ass  19128  ipcau  19148  nmpar  19150  fmcfil  19178  iscau3  19184  cmetcaulem  19194  cfilres  19202  bcthlem1  19230  bcthlem5  19234  cncdrg  19266  rlmbn  19268  cniccbdd  19311  ovolunnul  19349  ovolicc  19372  iundisj2  19396  ovolioo  19415  volcn  19451  itg1le  19558  itg2le  19584  iblcnlem  19633  dvfval  19737  dvid  19757  dvcnp2  19759  dvnf  19766  dvnbss  19767  dvn2bss  19769  evlsval2  19894  tdeglem3  19935  mdegldg  19942  mdegmullem  19954  deg1ldgdomn  19970  deg1lt  19973  deg1scl  19989  deg1mul3  19991  q1peqb  20030  fta1b  20045  elplyr  20073  ply1term  20076  dgrub  20106  coe1term  20130  dgradd2  20139  dgrmulc  20142  ofmulrt  20152  quotcl2  20172  quotdgr  20173  facth  20176  quotcan  20179  aannenlem1  20198  aannenlem2  20199  ulmf  20251  ptolemy  20357  tanord1  20392  efif1o  20401  argrege0  20459  logimul  20462  cxpneg  20525  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  ang180lem4  20607  isosctrlem2  20616  cxp2lim  20768  amgmlem  20781  wilthlem3  20806  sgmppw  20934  lgslem1  21033  lgsneg  21056  lgssq2  21073  lgsdirnn0  21076  lgsqrlem5  21082  lgsquad  21094  dirith  21176  pntrmax  21211  qrngdiv  21271  padicabv  21277  pthistrl  21525  isspthonpth  21537  1pthon  21544  grpoasscan2  21779  grpoinvop  21782  grpopncan  21792  grponpcan  21793  grpopnpcan2  21794  gxneg  21807  gxneg2  21808  gxcom  21810  gxinv  21811  gxsuc  21813  gxadd  21816  gxnn0mul  21818  gxmul  21819  gxmodid  21820  rngoass  21928  rngosn  21945  zerdivemp1  21975  nvpncan2  22090  nvaddsub4  22095  nvnncan  22097  nvdif  22107  nvpi  22108  nvz  22111  nvabs  22115  nv1  22118  imsmetlem  22135  4ipval2  22157  lnoadd  22212  isblo3i  22255  hvsubass  22499  shlub  22869  homco2  23433  leopmul2i  23591  mdslmd4i  23789  atexch  23837  atcvatlem  23841  cdj3lem2  23891  cdj3lem2a  23892  iundisj2f  23983  curry2ima  24050  supxrnemnf  24080  snunioc  24090  ubico  24091  iundisj2fi  24106  divnumden2  24114  xreceu  24121  xdivcl  24123  xdivrec  24126  xrge0addass  24164  ofldaddlt  24194  rhmdvd  24212  redvr  24230  cnre2csqlem  24261  relogbcl  24355  logb1  24356  logblt  24359  hasheuni  24428  sigaclcuni  24454  difelsiga  24469  elsigagen2  24484  sigagenss2  24486  measbase  24504  measval  24505  ismeas  24506  isrnmeas  24507  measxun2  24517  measun  24518  measvunilem  24519  measvuni  24521  mbfmco2  24568  dya2iocnrect  24584  probun  24630  probdif  24631  totprob  24638  probmeasb  24641  cndprobin  24645  cndprobnul  24648  ballotlemfrcn0  24740  erdszelem2  24831  cvmcov2  24915  dedekindle  25141  mulcan1g  25142  subdivcomb1  25148  dfon2lem2  25354  frrlem3  25497  brbtwn  25742  brbtwn2  25748  colinearalglem1  25749  colinearalglem2  25750  colinearalg  25753  axcgrid  25759  ax5seglem1  25771  ax5seglem2  25772  axpasch  25784  axlowdimlem16  25800  axcontlem4  25810  axcontlem7  25813  cgrrflx  25825  cgrcomim  25827  cgrtr  25830  cgrtr3  25832  cgrcoml  25834  cgrcomr  25835  cgrtriv  25840  cgrdegen  25842  cgrextend  25846  segconeq  25848  segconeu  25849  btwntriv2  25850  btwntriv1  25854  btwnintr  25857  btwnexch3  25858  btwnouttr2  25860  btwnouttr  25862  btwnexch  25863  funtransport  25869  btwnxfr  25894  colinearex  25898  colineartriv1  25905  colineartriv2  25906  colinearxfr  25913  lineext  25914  linecgr  25919  lineid  25921  idinside  25922  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem12  25936  btwnconn1lem14  25938  btwnconn3  25941  midofsegid  25942  segcon2  25943  seglerflx  25950  segletr  25952  outsidene1  25961  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsideofeq  25968  funray  25978  liness  25983  lineunray  25985  lineelsb2  25986  linecom  25988  linethru  25991  hilbert1.1  25992  bpolycl  26002  bpolydif  26005  areacirclem4  26183  areacirclem6  26186  areacirc  26187  elicc3  26210  clsun  26221  neiin  26225  finlocfin  26269  blbnd  26386  zerdivemp1x  26461  smprngopr  26552  isfldidl  26568  istopclsd  26644  ismrc  26645  mapco2g  26659  mapfzcons  26662  ofmpteq  26666  mzpcl34  26678  mzpexpmpt  26692  mzpsubst  26695  mzpresrename  26697  eldioph  26706  diophrw  26707  eqrabdioph  26726  lerabdioph  26755  ltrabdioph  26758  dvdsrabdioph  26760  diophren  26764  pellex  26788  pell14qrexpclnn0  26819  pellfundex  26839  rmxyadd  26874  rmyabs  26913  jm2.17a  26915  mzpcong  26927  acongeq  26938  coprmdvdsb  26942  modabsdifz  26946  jm2.22  26956  jm2.20nn  26958  rmxdiophlem  26976  rmxdioph  26977  jm3.1  26981  expdiophlem2  26983  islssfgi  27038  pwssplit0  27055  pwssplit1  27056  pwssplit2  27057  pwssplit3  27058  pwssplit4  27059  uvcresum  27110  frlmsplit2  27111  frlmsslss  27112  frlmup4  27121  islindf2  27152  lindsind2  27157  lindff1  27158  f1lindf  27160  lindsss  27162  f1linds  27163  cnsrexpcl  27238  pmtrfrn  27268  idomrootle  27379  fiuneneq  27381  ofdivrec  27411  ofdivcan4  27412  ubelsupr  27558  fnchoice  27567  fmul01  27577  fmuldfeq  27580  fmul01lt1lem2  27582  infrglb  27589  climsuse  27601  stoweidlem16  27632  stoweidlem20  27636  stoweidlem60  27676  wallispilem3  27683  sigaraf  27710  sigarmf  27711  sigaras  27712  sigarms  27713  sigarls  27714  sigarperm  27717  otiunsndisj  27954  otiunsndisjX  27955  leaddsuble  27970  nbfiusgrafi  28034  frg2woteu  28158  3orbi123  28305  alrim3con13v  28328  tratrb  28331  3orbi123VD  28671  19.21a3con13vVD  28673  tratrbVD  28682  bnj900  29006  bnj1110  29057  bnj1128  29065  bnj1125  29067  bnj1136  29072  bnj1189  29084  bnj1204  29087  bnj1321  29102  bnj1413  29110  lubunNEW  29456  lfladd  29549  lflsub  29550  lflmul  29551  lkrlsp2  29586  lshpkrlem5  29597  oplecon3b  29683  latm4  29716  omllaw4  29729  omllaw5N  29730  cmtcomlemN  29731  cmtbr2N  29736  cmtbr3N  29737  omlmod1i2N  29743  omlspjN  29744  cvrnbtwn3  29759  cvrcon3b  29760  cvrcmp  29766  cvrcmp2  29767  cvlatexch3  29821  cvlsupr5  29829  cvlsupr7  29831  hlrelat2  29885  2llnneN  29891  cvrval5  29897  cvrexch  29902  cvratlem  29903  atcvr0eq  29908  atcvrneN  29912  atcvrj1  29913  atle  29918  atlt  29919  atlelt  29920  2atjm  29927  3noncolr2  29931  3noncolr1N  29932  hlatcon2  29934  3dim1  29949  3dim2  29950  1cvratex  29955  1cvrat  29958  ps-1  29959  ps-2  29960  2atjlej  29961  hlatexch3N  29962  llnexatN  30003  llncmp  30004  lplni2  30019  lplnnle2at  30023  lplnnleat  30024  lplnri3N  30037  2lplnmN  30041  2llnmj  30042  lplncmp  30044  lplnexatN  30045  2llnm2N  30050  2llnm3N  30051  2llnmeqat  30053  2atnelvolN  30069  4atlem0ae  30076  4atlem0be  30077  4atlem3b  30080  4atlem9  30085  4atlem10a  30086  4atlem10  30088  lvolcmp  30099  2lplnm2N  30103  2lplnmj  30104  pmapglbx  30251  pmapmeet  30255  2llnma1b  30268  2llnma1  30269  2llnma3r  30270  2llnma2  30271  2llnma2rN  30272  elpadd2at  30288  paddasslem16  30317  padd4N  30322  paddclN  30324  pmodlem2  30329  pmapjoin  30334  pmapjat1  30335  pmapjat2  30336  hlmod1i  30338  atmod2i1  30343  atmod2i2  30344  atmod3i1  30346  llnexchb2  30351  dalawlem2  30354  elpcliN  30375  pclssN  30376  pclunN  30380  pclun2N  30381  polcon3N  30399  2polcon4bN  30400  paddunN  30409  poldmj1N  30410  pmapj2N  30411  pmapocjN  30412  psubclinN  30430  paddatclN  30431  poml5N  30436  osumcllem3N  30440  pexmidlem3N  30454  pexmidlem4N  30455  lhple  30524  lhpat4N  30526  4atex2  30559  4atex2-0bOLDN  30561  4atex3  30563  ltrnatb  30619  ltrnel  30621  ltrncnvel  30624  ltrncoelN  30625  ltrncoat  30626  ltrncoval  30627  ltrncnv  30628  ltrn11at  30629  ltrnmw  30633  trlcnv  30647  trljat2  30649  trlat  30651  trl0  30652  ltrnnidn  30656  trlnid  30661  trlval3  30669  trlval4  30670  cdlemc2  30674  cdlemc5  30677  cdlemc6  30678  cdlemd7  30686  cdleme00a  30691  cdleme0e  30699  cdleme01N  30703  cdleme02N  30704  cdleme0ex1N  30705  cdleme0ex2N  30706  cdleme3g  30716  cdleme3h  30717  cdleme3  30719  cdleme4  30720  cdleme5  30722  cdleme7b  30726  cdleme9  30735  cdleme11a  30742  cdleme11dN  30744  cdleme11e  30745  cdleme11g  30747  cdleme11h  30748  cdleme11j  30749  cdleme11k  30750  cdleme12  30753  cdleme18a  30773  cdleme18b  30774  cdleme18c  30775  cdleme22gb  30776  cdleme20zN  30783  cdleme20y  30784  cdleme19a  30785  cdleme20d  30794  cdleme20i  30799  cdleme20j  30800  cdleme20l2  30803  cdleme22a  30822  cdleme22d  30825  cdleme22e  30826  cdleme30a  30860  cdlemefs32sn1aw  30896  cdlemefs29bpre0N  30898  cdlemefs29bpre1N  30899  cdlemefs29cpre1N  30900  cdlemefs29clN  30901  cdleme43fsv1snlem  30902  cdlemefs32fvaN  30904  cdlemefs32fva1  30905  cdlemefs31fv1  30906  cdlemefs45eN  30913  cdleme41sn3a  30915  cdleme32fva  30919  cdleme32fvaw  30921  cdleme32b  30924  cdleme32c  30925  cdleme32e  30927  cdleme35h  30938  cdleme37m  30944  cdleme38m  30945  cdleme40m  30949  cdleme40n  30950  cdleme41sn3aw  30956  cdleme41sn4aw  30957  cdleme41fva11  30959  cdleme42b  30960  cdleme42e  30961  cdleme42h  30964  cdleme42i  30965  cdleme42k  30966  cdleme43cN  30973  cdleme17d2  30977  cdleme17d3  30978  cdleme48fv  30981  cdleme48bw  30984  cdleme48b  30985  cdlemeg47rv2  30992  cdlemeg46c  30995  cdlemeg46sfg  31002  cdlemeg46fjgN  31003  cdlemeg46rjgN  31004  cdlemeg46fjv  31005  cdlemeg46frv  31007  cdlemeg46vrg  31009  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfv  31012  cdlemeg46gfre  31014  cdleme48d  31017  cdlemeg49lebilem  31021  cdleme50trn2  31033  cdleme50ltrn  31039  ltrniotacnvval  31064  ltrniotavalbN  31066  cdlemg1cex  31070  cdlemg2dN  31072  cdlemg2fvlem  31076  cdlemg2fv2  31082  cdlemg2kq  31084  cdlemg2l  31085  cdlemg2m  31086  cdlemg4a  31090  cdlemg4b1  31091  cdlemg4b2  31092  cdlemg4d  31095  cdlemg4e  31096  cdlemg4f  31097  cdlemg4  31099  cdlemg6d  31103  cdlemg6e  31104  cdlemg7fvN  31106  cdlemg8a  31109  cdlemg8b  31110  cdlemg8c  31111  cdlemg9a  31114  cdlemg9b  31115  cdlemg9  31116  cdlemg11aq  31120  cdlemg10c  31121  cdlemg12a  31125  cdlemg12b  31126  cdlemg12c  31127  cdlemg12f  31130  cdlemg12g  31131  cdlemg14f  31135  cdlemg14g  31136  cdlemg17a  31143  cdlemg17dN  31145  cdlemg17e  31147  cdlemg17i  31151  cdlemg17ir  31152  cdlemg17  31159  cdlemg18b  31161  cdlemg18c  31162  cdlemg18d  31163  cdlemg18  31164  cdlemg21  31168  cdlemg28a  31175  cdlemg31b0a  31177  cdlemg31a  31179  cdlemg31b  31180  cdlemg28b  31185  cdlemg33c  31190  cdlemg33d  31191  cdlemg33e  31192  cdlemg35  31195  cdlemg41  31200  ltrnco  31201  trlcocnv  31202  trlcoabs  31203  trlcoabs2N  31204  trlcocnvat  31206  trlconid  31207  trlcolem  31208  trlcone  31210  cdlemg42  31211  cdlemg43  31212  cdlemg44a  31213  cdlemg47a  31216  cdlemg46  31217  trljco  31222  tendoset  31241  tendof  31245  tendoeq1  31246  tendocoval  31248  tendoco2  31250  tendococl  31254  tendoplcl2  31260  tendoplco2  31261  tendopltp  31262  tendoplcl  31263  tendoplcom  31264  cdlemh  31299  cdlemi1  31300  cdlemi2  31301  cdlemk1  31313  cdlemk2  31314  cdlemk3  31315  cdlemk4  31316  cdlemk8  31320  cdlemk9  31321  cdlemk9bN  31322  cdlemki  31323  cdlemkvcl  31324  cdlemk10  31325  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemk5u  31343  cdlemk6u  31344  cdlemk7u  31352  cdlemk12u  31354  cdlemk22  31375  cdlemk32  31379  cdlemk28-3  31390  cdlemk34  31392  cdlemk29-3  31393  cdlemk39  31398  cdlemkfid1N  31403  cdlemkid1  31404  cdlemkid2  31406  cdlemkfid3N  31407  cdlemk54  31440  cdlemk19u  31452  cdlemk56w  31455  tendoex  31457  cdleml1N  31458  cdleml2N  31459  cdleml3N  31460  cdleml6  31463  cdleml7  31464  cdleml8  31465  cdleml9  31466  tendocnv  31504  tendospcanN  31506  dvhopvadd  31576  tendolinv  31588  tendorinv  31589  dicvaddcl  31673  dicvscacl  31674  cdlemn2  31678  cdlemn2a  31679  cdlemn3  31680  cdlemn4  31681  cdlemn4a  31682  cdlemn5pre  31683  cdlemn6  31685  cdlemn7  31686  cdlemn8  31687  cdlemn9  31688  cdlemn10  31689  cdlemn11a  31690  cdlemn11c  31692  cdlemn11pre  31693  dihordlem6  31696  dihordlem7  31697  dihordlem7b  31698  dihjustlem  31699  dihjust  31700  dihord2cN  31704  dihord11c  31707  dihvalcq2  31730  dihopelvalcpre  31731  dihmeetlem1N  31773  dihglblem3N  31778  dihmeetlem2N  31782  dihglbcpreN  31783  dihmeetcN  31785  dihmeetbclemN  31787  dihmeetlem4preN  31789  dihmeetlem9N  31798  dihmeetlem13N  31802  dihmeetlem20N  31809  dih1dimatlem0  31811  dihlspsnat  31816  dihmeet  31826  dochss  31848  dochdmj1  31873  hdmap1fval  32280  hdmapfval  32313  hgmapfval  32372
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