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  2733  funtpg  5464  feq123  5547  fresaun  5577  foco2  5852  ftpg  5879  fsnunf  5894  fsnunf2  5895  fnsuppres  5915  fcofo  5984  fveqf1o  5992  f1oiso2  6035  ovmpt2x  6165  ovmpt2ga  6166  ofeq  6270  ofrval  6278  riotass  6541  riotasv2s  6559  onoviun  6568  omwordri  6778  omeulem1  6788  oeord  6794  oewordri  6798  oeordsuc  6800  erov  6964  mapxpen  7236  unbnn  7326  fofinf1o  7350  elfir  7382  inelfi  7385  dffi2  7390  elfiun  7397  fisup2g  7431  suppr  7433  ordtype2  7463  hartogslem1  7471  wemapso  7480  wemapso2  7481  ixpiunwdom  7519  cnfcom3clem  7622  cdaassen  8022  mapcdaen  8024  infcdaabs  8046  infunabs  8047  infdif  8049  infdif2  8050  cfsmolem  8110  isf32lem11  8203  isf34lem7  8219  zornn0g  8345  ttukey2g  8356  konigthlem  8403  gchdomtri  8464  fpwwe  8481  canthwe  8486  gchaleph  8510  gchaleph2  8511  winainflem  8528  wununi  8541  tsksuc  8597  tskpr  8605  tskop  8606  tskcard  8616  grupw  8630  grurn  8636  gruop  8640  gruun  8641  grumap  8643  gruixp  8644  distrlem4pr  8863  ltadd2  9137  mul31  9194  readdcan  9200  addid2  9209  addsubass  9275  subcan2  9286  subsub2  9289  subsub4  9294  npncan3  9299  pnpcan  9300  pnncan  9302  subcan  9316  subdi  9427  ltadd1  9455  leadd1  9456  leadd2  9457  ltsubadd  9458  lesubadd  9460  lesub1  9482  lesub2  9483  ltsub1  9484  ltsub2  9485  mulcan  9619  mulcan2  9620  divcan2  9646  diveq0  9648  divrec  9654  divrec2  9655  divdir  9661  divcan3  9662  div11  9664  divcan5  9676  redivcl  9693  div2neg  9697  ltmul1  9820  ltdiv1  9834  ltmuldiv  9840  ledivmulOLD  9844  lemuldiv  9849  lt2msq1  9853  suprub  9929  suprlub  9930  infmsup  9946  infmrgelb  9948  infmrlb  9949  ofsubeq0  9957  ofnegsub  9958  ofsubge0  9959  gtndiv  10307  eluz2  10454  peano2uz  10490  suprzub  10527  xrltmin  10730  xrlemin  10732  xaddass  10788  xleadd1  10794  xltadd1  10795  xmulass  10826  xlemul1  10829  xlemul2  10830  xltmul1  10831  xadddi  10834  xadddir  10835  xadddi2  10836  supxrre  10866  infmxrre  10874  ixxssixx  10890  ixxub  10897  ixxlb  10898  lbico1  10926  lbicc2  10973  icoshftf1o  10980  snunioo  10983  snunico  10984  iccsplit  10989  fzrev3  11071  fzm1  11086  fzrevral2  11091  elfzo0  11130  flwordi  11178  flword2  11179  expgt1  11377  exprec  11380  leexp2a  11394  expubnd  11399  sqdiv  11406  expnbnd  11467  expmulnbnd  11470  modexp  11473  bccmpl  11559  ccatass  11709  swrdval  11723  swrdval2  11726  ccatco  11763  s3cl  11800  swrds2  11839  mulre  11885  caubnd  12121  climuni  12305  iseraltlem3  12436  geoisum1c  12616  eflt  12677  rpnnen2lem4  12776  dvdsmultr2  12844  dvdsexp  12864  sadass  12942  dvdsgcdb  13003  gcdass  13004  mulgcd  13005  gcddiv  13008  rplpwr  13015  coprmdvds  13061  mulgcddvds  13063  qredeq  13065  rpexp12i  13081  rpmul  13082  odzcllem  13137  odzphi  13141  pythagtriplem15  13162  pcpremul  13176  pcdiv  13185  pcqmul  13186  pcqdiv  13190  vdwapfval  13298  vdwapun  13301  vdwpc  13307  hashbcss  13331  ramval  13335  0ram2  13348  0ramcl  13350  ramcl  13356  ressbas  13478  xpsadd  13760  xpsmul  13761  mreiincl  13780  mreincl  13783  mrcss  13800  mrcun  13806  submrc  13812  posasymb  14368  meetle  14416  p0le  14431  ple1  14432  latleeqj1  14451  latjlej12  14455  latleeqm1  14467  latmlem12  14471  latnlemlt  14472  latj4  14489  latj4rot  14490  lubss  14507  lubun  14509  clatglbss  14513  pospropd  14520  isipodrs  14546  imasmnd2  14691  gsumccat  14746  frmdup3  14770  grpinvadd  14826  grpsubeq0  14834  grppncan  14838  grpsubpropd2  14849  pwsinvg  14889  imasgrp2  14892  issubg  14903  nsgconj  14932  nsgid  14945  ghmnsgima  14988  odcong  15146  isslw  15201  pgpssslw  15207  lsmsubg  15247  efgsval2  15324  frgpup3  15369  cmn4  15390  ablinvadd  15393  ablsub4  15396  abladdsub4  15397  ablpncan2  15399  lsmsubg2  15433  lsm4  15434  rngcom  15651  imasrng  15684  unitmulcl  15728  unitmulclb  15729  dvrcan1  15755  dvrcan3  15756  irredrmul  15771  isabvd  15867  abvdom  15885  islmod  15913  lmodcom  15949  lss0cl  15982  lssvnegcl  15991  lssincl  16000  lspss  16019  lspun  16022  lspsnvsi  16039  lsslsp  16050  lmodvsinv  16071  lmodvsinv2  16072  0lmhm  16075  lsmsp  16117  lsmsp2  16118  lspvadd  16127  lspsntri  16128  lidldvgen  16285  rrgeq0  16309  aspid  16348  aspss  16350  asclmul1  16357  asclmul2  16358  psrbagaddcl  16394  psrbagconcl  16397  coe1tm  16624  coe1sclmul  16633  coe1sclmul2  16635  phllmhm  16822  ip2eq  16843  cssmre  16879  iuncld  17068  clsss  17077  ntrin  17084  clsndisj  17098  iscldtop  17118  neiss  17132  lpss3  17167  restco  17186  restabs  17187  restcldi  17195  neitr  17202  restcls  17203  restntr  17204  restlp  17205  lmconst  17283  cnpresti  17310  hausnei2  17375  sshauslem  17394  clscon  17450  concompss  17453  concompclo  17455  kgen2ss  17544  elptr  17562  xkococn  17649  qtopval2  17685  qtoptop2  17688  cmphaushmeo  17789  elmptrab  17816  filinn0  17849  fbasweak  17854  snfbas  17855  filuni  17874  trnei  17881  fmval  17932  rnelfm  17942  flimrest  17972  flimclslem  17973  flfnei  17980  isflf  17982  lmflf  17994  fclsneii  18006  fclsrest  18013  isfcf  18023  ptcmpg  18045  istgp2  18078  divstgpopn  18106  divstgphaus  18109  ustfn  18188  ustval  18189  isust  18190  ustssel  18192  ustn0  18207  trust  18216  utop2nei  18237  ressusp  18252  trcfilu  18281  cfiluweak  18282  psmetsym  18298  psmetge0  18300  xmetge0  18331  xmetsym  18334  xmetresbl  18424  mopni3  18481  stdbdxmet  18502  stdbdmopn  18505  prdsxms  18517  prdsms  18518  metustblOLD  18567  metustbl  18568  xmsuspOLD  18572  xmsusp  18573  restmetu  18574  isngp4  18615  nmsub  18626  nm2dif  18628  nminvr  18662  nmoix  18720  nmods  18735  metds0  18837  metnrm  18849  cncfmptc  18898  iirev  18911  icoopnst  18921  iocopnst  18922  icchmeo  18923  iccpnfhmeo  18927  pi1blem  19021  isclmi  19059  cphsqrcl  19104  cph2ass  19132  ipcau  19152  nmpar  19154  fmcfil  19182  iscau3  19188  cmetcaulem  19198  cfilres  19206  bcthlem1  19234  bcthlem5  19238  cncdrg  19270  rlmbn  19272  cniccbdd  19315  ovolunnul  19353  ovolicc  19376  iundisj2  19400  ovolioo  19419  volcn  19455  itg1le  19562  itg2le  19588  iblcnlem  19637  dvfval  19741  dvid  19761  dvcnp2  19763  dvnf  19770  dvnbss  19771  dvn2bss  19773  evlsval2  19898  tdeglem3  19939  mdegldg  19946  mdegmullem  19958  deg1ldgdomn  19974  deg1lt  19977  deg1scl  19993  deg1mul3  19995  q1peqb  20034  fta1b  20049  elplyr  20077  ply1term  20080  dgrub  20110  coe1term  20134  dgradd2  20143  dgrmulc  20146  ofmulrt  20156  quotcl2  20176  quotdgr  20177  facth  20180  quotcan  20183  aannenlem1  20202  aannenlem2  20203  ulmf  20255  ptolemy  20361  tanord1  20396  efif1o  20405  argrege0  20463  logimul  20466  cxpneg  20529  ang180lem1  20608  ang180lem2  20609  ang180lem3  20610  ang180lem4  20611  isosctrlem2  20620  cxp2lim  20772  amgmlem  20785  wilthlem3  20810  sgmppw  20938  lgslem1  21037  lgsneg  21060  lgssq2  21077  lgsdirnn0  21080  lgsqrlem5  21086  lgsquad  21098  dirith  21180  pntrmax  21215  qrngdiv  21275  padicabv  21281  pthistrl  21529  isspthonpth  21541  1pthon  21548  grpoasscan2  21783  grpoinvop  21786  grpopncan  21796  grponpcan  21797  grpopnpcan2  21798  gxneg  21811  gxneg2  21812  gxcom  21814  gxinv  21815  gxsuc  21817  gxadd  21820  gxnn0mul  21822  gxmul  21823  gxmodid  21824  rngoass  21932  rngosn  21949  zerdivemp1  21979  nvpncan2  22094  nvaddsub4  22099  nvnncan  22101  nvdif  22111  nvpi  22112  nvz  22115  nvabs  22119  nv1  22122  imsmetlem  22139  4ipval2  22161  lnoadd  22216  isblo3i  22259  hvsubass  22503  shlub  22873  homco2  23437  leopmul2i  23595  mdslmd4i  23793  atexch  23841  atcvatlem  23845  cdj3lem2  23895  cdj3lem2a  23896  iundisj2f  23987  curry2ima  24054  supxrnemnf  24084  snunioc  24094  ubico  24095  iundisj2fi  24110  divnumden2  24118  xreceu  24125  xdivcl  24127  xdivrec  24130  xrge0addass  24168  ofldaddlt  24198  rhmdvd  24216  redvr  24234  cnre2csqlem  24265  relogbcl  24359  logb1  24360  logblt  24363  hasheuni  24432  sigaclcuni  24458  difelsiga  24473  elsigagen2  24488  sigagenss2  24490  measbase  24508  measval  24509  ismeas  24510  isrnmeas  24511  measxun2  24521  measun  24522  measvunilem  24523  measvuni  24525  mbfmco2  24572  dya2iocnrect  24588  probun  24634  probdif  24635  totprob  24642  probmeasb  24645  cndprobin  24649  cndprobnul  24652  ballotlemfrcn0  24744  erdszelem2  24835  cvmcov2  24919  dedekindle  25145  mulcan1g  25146  subdivcomb1  25152  dfon2lem2  25358  frrlem3  25501  brbtwn  25746  brbtwn2  25752  colinearalglem1  25753  colinearalglem2  25754  colinearalg  25757  axcgrid  25763  ax5seglem1  25775  ax5seglem2  25776  axpasch  25788  axlowdimlem16  25804  axcontlem4  25814  axcontlem7  25817  cgrrflx  25829  cgrcomim  25831  cgrtr  25834  cgrtr3  25836  cgrcoml  25838  cgrcomr  25839  cgrtriv  25844  cgrdegen  25846  cgrextend  25850  segconeq  25852  segconeu  25853  btwntriv2  25854  btwntriv1  25858  btwnintr  25861  btwnexch3  25862  btwnouttr2  25864  btwnouttr  25866  btwnexch  25867  funtransport  25873  btwnxfr  25898  colinearex  25902  colineartriv1  25909  colineartriv2  25910  colinearxfr  25917  lineext  25918  linecgr  25923  lineid  25925  idinside  25926  btwnconn1lem7  25935  btwnconn1lem8  25936  btwnconn1lem9  25937  btwnconn1lem12  25940  btwnconn1lem14  25942  btwnconn3  25945  midofsegid  25946  segcon2  25947  seglerflx  25954  segletr  25956  outsidene1  25965  btwnoutside  25967  broutsideof3  25968  outsideoftr  25971  outsideofeq  25972  funray  25982  liness  25987  lineunray  25989  lineelsb2  25990  linecom  25992  linethru  25995  hilbert1.1  25996  bpolycl  26006  bpolydif  26009  areacirclem4  26187  areacirclem6  26190  areacirc  26191  elicc3  26214  clsun  26225  neiin  26229  finlocfin  26273  blbnd  26390  zerdivemp1x  26465  smprngopr  26556  isfldidl  26572  istopclsd  26648  ismrc  26649  mapco2g  26663  mapfzcons  26666  ofmpteq  26670  mzpcl34  26682  mzpexpmpt  26696  mzpsubst  26699  mzpresrename  26701  eldioph  26710  diophrw  26711  eqrabdioph  26730  lerabdioph  26759  ltrabdioph  26762  dvdsrabdioph  26764  diophren  26768  pellex  26792  pell14qrexpclnn0  26823  pellfundex  26843  rmxyadd  26878  rmyabs  26917  jm2.17a  26919  mzpcong  26931  acongeq  26942  coprmdvdsb  26946  modabsdifz  26950  jm2.22  26960  jm2.20nn  26962  rmxdiophlem  26980  rmxdioph  26981  jm3.1  26985  expdiophlem2  26987  islssfgi  27042  pwssplit0  27059  pwssplit1  27060  pwssplit2  27061  pwssplit3  27062  pwssplit4  27063  uvcresum  27114  frlmsplit2  27115  frlmsslss  27116  frlmup4  27125  islindf2  27156  lindsind2  27161  lindff1  27162  f1lindf  27164  lindsss  27166  f1linds  27167  cnsrexpcl  27242  pmtrfrn  27272  idomrootle  27383  fiuneneq  27385  ofdivrec  27415  ofdivcan4  27416  ubelsupr  27562  fnchoice  27571  fmul01  27581  fmuldfeq  27584  fmul01lt1lem2  27586  infrglb  27593  climsuse  27605  stoweidlem16  27636  stoweidlem20  27640  stoweidlem60  27680  wallispilem3  27687  sigaraf  27714  sigarmf  27715  sigaras  27716  sigarms  27717  sigarls  27718  sigarperm  27721  otiunsndisj  27958  otiunsndisjX  27959  leaddsuble  27974  nbfiusgrafi  28038  frg2woteu  28162  3orbi123  28309  alrim3con13v  28332  tratrb  28335  3orbi123VD  28675  19.21a3con13vVD  28677  tratrbVD  28686  bnj900  29010  bnj1110  29061  bnj1128  29069  bnj1125  29071  bnj1136  29076  bnj1189  29088  bnj1204  29091  bnj1321  29106  bnj1413  29114  lubunNEW  29460  lfladd  29553  lflsub  29554  lflmul  29555  lkrlsp2  29590  lshpkrlem5  29601  oplecon3b  29687  latm4  29720  omllaw4  29733  omllaw5N  29734  cmtcomlemN  29735  cmtbr2N  29740  cmtbr3N  29741  omlmod1i2N  29747  omlspjN  29748  cvrnbtwn3  29763  cvrcon3b  29764  cvrcmp  29770  cvrcmp2  29771  cvlatexch3  29825  cvlsupr5  29833  cvlsupr7  29835  hlrelat2  29889  2llnneN  29895  cvrval5  29901  cvrexch  29906  cvratlem  29907  atcvr0eq  29912  atcvrneN  29916  atcvrj1  29917  atle  29922  atlt  29923  atlelt  29924  2atjm  29931  3noncolr2  29935  3noncolr1N  29936  hlatcon2  29938  3dim1  29953  3dim2  29954  1cvratex  29959  1cvrat  29962  ps-1  29963  ps-2  29964  2atjlej  29965  hlatexch3N  29966  llnexatN  30007  llncmp  30008  lplni2  30023  lplnnle2at  30027  lplnnleat  30028  lplnri3N  30041  2lplnmN  30045  2llnmj  30046  lplncmp  30048  lplnexatN  30049  2llnm2N  30054  2llnm3N  30055  2llnmeqat  30057  2atnelvolN  30073  4atlem0ae  30080  4atlem0be  30081  4atlem3b  30084  4atlem9  30089  4atlem10a  30090  4atlem10  30092  lvolcmp  30103  2lplnm2N  30107  2lplnmj  30108  pmapglbx  30255  pmapmeet  30259  2llnma1b  30272  2llnma1  30273  2llnma3r  30274  2llnma2  30275  2llnma2rN  30276  elpadd2at  30292  paddasslem16  30321  padd4N  30326  paddclN  30328  pmodlem2  30333  pmapjoin  30338  pmapjat1  30339  pmapjat2  30340  hlmod1i  30342  atmod2i1  30347  atmod2i2  30348  atmod3i1  30350  llnexchb2  30355  dalawlem2  30358  elpcliN  30379  pclssN  30380  pclunN  30384  pclun2N  30385  polcon3N  30403  2polcon4bN  30404  paddunN  30413  poldmj1N  30414  pmapj2N  30415  pmapocjN  30416  psubclinN  30434  paddatclN  30435  poml5N  30440  osumcllem3N  30444  pexmidlem3N  30458  pexmidlem4N  30459  lhple  30528  lhpat4N  30530  4atex2  30563  4atex2-0bOLDN  30565  4atex3  30567  ltrnatb  30623  ltrnel  30625  ltrncnvel  30628  ltrncoelN  30629  ltrncoat  30630  ltrncoval  30631  ltrncnv  30632  ltrn11at  30633  ltrnmw  30637  trlcnv  30651  trljat2  30653  trlat  30655  trl0  30656  ltrnnidn  30660  trlnid  30665  trlval3  30673  trlval4  30674  cdlemc2  30678  cdlemc5  30681  cdlemc6  30682  cdlemd7  30690  cdleme00a  30695  cdleme0e  30703  cdleme01N  30707  cdleme02N  30708  cdleme0ex1N  30709  cdleme0ex2N  30710  cdleme3g  30720  cdleme3h  30721  cdleme3  30723  cdleme4  30724  cdleme5  30726  cdleme7b  30730  cdleme9  30739  cdleme11a  30746  cdleme11dN  30748  cdleme11e  30749  cdleme11g  30751  cdleme11h  30752  cdleme11j  30753  cdleme11k  30754  cdleme12  30757  cdleme18a  30777  cdleme18b  30778  cdleme18c  30779  cdleme22gb  30780  cdleme20zN  30787  cdleme20y  30788  cdleme19a  30789  cdleme20d  30798  cdleme20i  30803  cdleme20j  30804  cdleme20l2  30807  cdleme22a  30826  cdleme22d  30829  cdleme22e  30830  cdleme30a  30864  cdlemefs32sn1aw  30900  cdlemefs29bpre0N  30902  cdlemefs29bpre1N  30903  cdlemefs29cpre1N  30904  cdlemefs29clN  30905  cdleme43fsv1snlem  30906  cdlemefs32fvaN  30908  cdlemefs32fva1  30909  cdlemefs31fv1  30910  cdlemefs45eN  30917  cdleme41sn3a  30919  cdleme32fva  30923  cdleme32fvaw  30925  cdleme32b  30928  cdleme32c  30929  cdleme32e  30931  cdleme35h  30942  cdleme37m  30948  cdleme38m  30949  cdleme40m  30953  cdleme40n  30954  cdleme41sn3aw  30960  cdleme41sn4aw  30961  cdleme41fva11  30963  cdleme42b  30964  cdleme42e  30965  cdleme42h  30968  cdleme42i  30969  cdleme42k  30970  cdleme43cN  30977  cdleme17d2  30981  cdleme17d3  30982  cdleme48fv  30985  cdleme48bw  30988  cdleme48b  30989  cdlemeg47rv2  30996  cdlemeg46c  30999  cdlemeg46sfg  31006  cdlemeg46fjgN  31007  cdlemeg46rjgN  31008  cdlemeg46fjv  31009  cdlemeg46frv  31011  cdlemeg46vrg  31013  cdlemeg46rgv  31014  cdlemeg46req  31015  cdlemeg46gfv  31016  cdlemeg46gfre  31018  cdleme48d  31021  cdlemeg49lebilem  31025  cdleme50trn2  31037  cdleme50ltrn  31043  ltrniotacnvval  31068  ltrniotavalbN  31070  cdlemg1cex  31074  cdlemg2dN  31076  cdlemg2fvlem  31080  cdlemg2fv2  31086  cdlemg2kq  31088  cdlemg2l  31089  cdlemg2m  31090  cdlemg4a  31094  cdlemg4b1  31095  cdlemg4b2  31096  cdlemg4d  31099  cdlemg4e  31100  cdlemg4f  31101  cdlemg4  31103  cdlemg6d  31107  cdlemg6e  31108  cdlemg7fvN  31110  cdlemg8a  31113  cdlemg8b  31114  cdlemg8c  31115  cdlemg9a  31118  cdlemg9b  31119  cdlemg9  31120  cdlemg11aq  31124  cdlemg10c  31125  cdlemg12a  31129  cdlemg12b  31130  cdlemg12c  31131  cdlemg12f  31134  cdlemg12g  31135  cdlemg14f  31139  cdlemg14g  31140  cdlemg17a  31147  cdlemg17dN  31149  cdlemg17e  31151  cdlemg17i  31155  cdlemg17ir  31156  cdlemg17  31163  cdlemg18b  31165  cdlemg18c  31166  cdlemg18d  31167  cdlemg18  31168  cdlemg21  31172  cdlemg28a  31179  cdlemg31b0a  31181  cdlemg31a  31183  cdlemg31b  31184  cdlemg28b  31189  cdlemg33c  31194  cdlemg33d  31195  cdlemg33e  31196  cdlemg35  31199  cdlemg41  31204  ltrnco  31205  trlcocnv  31206  trlcoabs  31207  trlcoabs2N  31208  trlcocnvat  31210  trlconid  31211  trlcolem  31212  trlcone  31214  cdlemg42  31215  cdlemg43  31216  cdlemg44a  31217  cdlemg47a  31220  cdlemg46  31221  trljco  31226  tendoset  31245  tendof  31249  tendoeq1  31250  tendocoval  31252  tendoco2  31254  tendococl  31258  tendoplcl2  31264  tendoplco2  31265  tendopltp  31266  tendoplcl  31267  tendoplcom  31268  cdlemh  31303  cdlemi1  31304  cdlemi2  31305  cdlemk1  31317  cdlemk2  31318  cdlemk3  31319  cdlemk4  31320  cdlemk8  31324  cdlemk9  31325  cdlemk9bN  31326  cdlemki  31327  cdlemkvcl  31328  cdlemk10  31329  cdlemksv2  31333  cdlemk7  31334  cdlemk11  31335  cdlemk12  31336  cdlemk5u  31347  cdlemk6u  31348  cdlemk7u  31356  cdlemk12u  31358  cdlemk22  31379  cdlemk32  31383  cdlemk28-3  31394  cdlemk34  31396  cdlemk29-3  31397  cdlemk39  31402  cdlemkfid1N  31407  cdlemkid1  31408  cdlemkid2  31410  cdlemkfid3N  31411  cdlemk54  31444  cdlemk19u  31456  cdlemk56w  31459  tendoex  31461  cdleml1N  31462  cdleml2N  31463  cdleml3N  31464  cdleml6  31467  cdleml7  31468  cdleml8  31469  cdleml9  31470  tendocnv  31508  tendospcanN  31510  dvhopvadd  31580  tendolinv  31592  tendorinv  31593  dicvaddcl  31677  dicvscacl  31678  cdlemn2  31682  cdlemn2a  31683  cdlemn3  31684  cdlemn4  31685  cdlemn4a  31686  cdlemn5pre  31687  cdlemn6  31689  cdlemn7  31690  cdlemn8  31691  cdlemn9  31692  cdlemn10  31693  cdlemn11a  31694  cdlemn11c  31696  cdlemn11pre  31697  dihordlem6  31700  dihordlem7  31701  dihordlem7b  31702  dihjustlem  31703  dihjust  31704  dihord2cN  31708  dihord11c  31711  dihvalcq2  31734  dihopelvalcpre  31735  dihmeetlem1N  31777  dihglblem3N  31782  dihmeetlem2N  31786  dihglbcpreN  31787  dihmeetcN  31789  dihmeetbclemN  31791  dihmeetlem4preN  31793  dihmeetlem9N  31802  dihmeetlem13N  31806  dihmeetlem20N  31813  dih1dimatlem0  31815  dihlspsnat  31820  dihmeet  31830  dochss  31852  dochdmj1  31877  hdmap1fval  32284  hdmapfval  32317  hgmapfval  32376
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