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

Theorem simp1 958
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 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ( ph  /\  ps ) )
21simpld 447 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simpl1  961  simpr1  964  simp1i  967  simp1d  970  simp11  988  simp21  991  simp31  994  syld3an3  1230  intn3an1d  1294  rsp2e  2771  funtpg  5504  feq123  5587  fresaun  5617  foco2  5892  ftpg  5919  fsnunf  5934  fsnunf2  5935  fnsuppres  5955  fcofo  6024  fveqf1o  6032  f1oiso2  6075  ovmpt2x  6205  ovmpt2ga  6206  ofeq  6310  ofrval  6318  riotass  6581  riotasv2s  6599  onoviun  6608  omwordri  6818  omeulem1  6828  oeord  6834  oewordri  6838  oeordsuc  6840  erov  7004  mapxpen  7276  unbnn  7366  fofinf1o  7390  elfir  7423  inelfi  7426  dffi2  7431  elfiun  7438  fisup2g  7474  suppr  7476  ordtype2  7506  hartogslem1  7514  wemapso  7523  wemapso2  7524  ixpiunwdom  7562  cnfcom3clem  7665  cdaassen  8067  mapcdaen  8069  infcdaabs  8091  infunabs  8092  infdif  8094  infdif2  8095  cfsmolem  8155  isf32lem11  8248  isf34lem7  8264  zornn0g  8390  ttukey2g  8401  konigthlem  8448  gchdomtri  8509  fpwwe  8526  canthwe  8531  gchaleph  8551  gchaleph2  8552  winainflem  8573  wununi  8586  tsksuc  8642  tskpr  8650  tskop  8651  tskcard  8661  grupw  8675  grurn  8681  gruop  8685  gruun  8686  grumap  8688  gruixp  8689  distrlem4pr  8908  ltadd2  9182  mul31  9239  readdcan  9245  addid2  9254  addsubass  9320  subcan2  9331  subsub2  9334  subsub4  9339  npncan3  9344  pnpcan  9345  pnncan  9347  subcan  9361  subdi  9472  ltadd1  9500  leadd1  9501  leadd2  9502  ltsubadd  9503  lesubadd  9505  lesub1  9527  lesub2  9528  ltsub1  9529  ltsub2  9530  mulcan  9664  mulcan2  9665  divcan2  9691  diveq0  9693  divrec  9699  divrec2  9700  divdir  9706  divcan3  9707  div11  9709  divcan5  9721  redivcl  9738  div2neg  9742  ltmul1  9865  ltdiv1  9879  ltmuldiv  9885  ledivmulOLD  9889  lemuldiv  9894  lt2msq1  9898  suprub  9974  suprlub  9975  infmsup  9991  infmrgelb  9993  infmrlb  9994  ofsubeq0  10002  ofnegsub  10003  ofsubge0  10004  gtndiv  10352  eluz2  10499  peano2uz  10535  suprzub  10572  xrltmin  10775  xrlemin  10777  xaddass  10833  xleadd1  10839  xltadd1  10840  xmulass  10871  xlemul1  10874  xlemul2  10875  xltmul1  10876  xadddi  10879  xadddir  10880  xadddi2  10881  supxrre  10911  infmxrre  10919  ixxssixx  10935  ixxub  10942  ixxlb  10943  lbico1  10971  lbicc2  11018  icoshftf1o  11025  snunioo  11028  snunico  11029  iccsplit  11034  fzrev3  11116  fzm1  11132  fzrevral2  11137  elfzo0  11176  flwordi  11224  flword2  11225  expgt1  11423  exprec  11426  leexp2a  11440  expubnd  11445  sqdiv  11452  expnbnd  11513  expmulnbnd  11516  modexp  11519  bccmpl  11605  ccatass  11755  swrdval  11769  swrdval2  11772  ccatco  11809  s3cl  11846  swrds2  11885  mulre  11931  caubnd  12167  climuni  12351  iseraltlem3  12482  geoisum1c  12662  eflt  12723  rpnnen2lem4  12822  dvdsmultr2  12890  dvdsexp  12910  sadass  12988  dvdsgcdb  13049  gcdass  13050  mulgcd  13051  gcddiv  13054  rplpwr  13061  coprmdvds  13107  mulgcddvds  13109  qredeq  13111  rpexp12i  13127  rpmul  13128  odzcllem  13183  odzphi  13187  pythagtriplem15  13208  pcpremul  13222  pcdiv  13231  pcqmul  13232  pcqdiv  13236  vdwapfval  13344  vdwapun  13347  vdwpc  13353  hashbcss  13377  ramval  13381  0ram2  13394  0ramcl  13396  ramcl  13402  ressbas  13524  xpsadd  13806  xpsmul  13807  mreiincl  13826  mreincl  13829  mrcss  13846  mrcun  13852  submrc  13858  posasymb  14414  meetle  14462  p0le  14477  ple1  14478  latleeqj1  14497  latjlej12  14501  latleeqm1  14513  latmlem12  14517  latnlemlt  14518  latj4  14535  latj4rot  14536  lubss  14553  lubun  14555  clatglbss  14559  pospropd  14566  isipodrs  14592  imasmnd2  14737  gsumccat  14792  frmdup3  14816  grpinvadd  14872  grpsubeq0  14880  grppncan  14884  grpsubpropd2  14895  pwsinvg  14935  imasgrp2  14938  issubg  14949  nsgconj  14978  nsgid  14991  ghmnsgima  15034  odcong  15192  isslw  15247  pgpssslw  15253  lsmsubg  15293  efgsval2  15370  frgpup3  15415  cmn4  15436  ablinvadd  15439  ablsub4  15442  abladdsub4  15443  ablpncan2  15445  lsmsubg2  15479  lsm4  15480  rngcom  15697  imasrng  15730  unitmulcl  15774  unitmulclb  15775  dvrcan1  15801  dvrcan3  15802  irredrmul  15817  isabvd  15913  abvdom  15931  islmod  15959  lmodcom  15995  lss0cl  16028  lssvnegcl  16037  lssincl  16046  lspss  16065  lspun  16068  lspsnvsi  16085  lsslsp  16096  lmodvsinv  16117  lmodvsinv2  16118  0lmhm  16121  lsmsp  16163  lsmsp2  16164  lspvadd  16173  lspsntri  16174  lidldvgen  16331  rrgeq0  16355  aspid  16394  aspss  16396  asclmul1  16403  asclmul2  16404  psrbagaddcl  16440  psrbagconcl  16443  coe1tm  16670  coe1sclmul  16679  coe1sclmul2  16681  phllmhm  16868  ip2eq  16889  cssmre  16925  iuncld  17114  clsss  17123  ntrin  17130  clsndisj  17144  iscldtop  17164  neiss  17178  lpss3  17213  restco  17233  restabs  17234  restcldi  17242  neitr  17249  restcls  17250  restntr  17251  restlp  17252  lmconst  17330  cnpresti  17357  hausnei2  17422  sshauslem  17441  bwth  17478  clscon  17498  concompss  17501  concompclo  17503  kgen2ss  17592  elptr  17610  xkococn  17697  qtopval2  17733  qtoptop2  17736  cmphaushmeo  17837  elmptrab  17864  filinn0  17897  fbasweak  17902  snfbas  17903  filuni  17922  trnei  17929  fmval  17980  rnelfm  17990  flimrest  18020  flimclslem  18021  flfnei  18028  isflf  18030  lmflf  18042  fclsneii  18054  fclsrest  18061  isfcf  18071  ptcmpg  18093  istgp2  18126  divstgpopn  18154  divstgphaus  18157  ustfn  18236  ustval  18237  isust  18238  ustssel  18240  ustn0  18255  trust  18264  utop2nei  18285  ressusp  18300  trcfilu  18329  cfiluweak  18330  psmetsym  18346  psmetge0  18348  xmetge0  18379  xmetsym  18382  xmetresbl  18472  mopni3  18529  stdbdxmet  18550  stdbdmopn  18553  prdsxms  18565  prdsms  18566  metustblOLD  18615  metustbl  18616  xmsuspOLD  18620  xmsusp  18621  restmetu  18622  isngp4  18663  nmsub  18674  nm2dif  18676  nminvr  18710  nmoix  18768  nmods  18783  metds0  18885  metnrm  18897  cncfmptc  18946  iirev  18959  icoopnst  18969  iocopnst  18970  icchmeo  18971  iccpnfhmeo  18975  pi1blem  19069  isclmi  19107  cphsqrcl  19152  cph2ass  19180  ipcau  19200  nmpar  19202  fmcfil  19230  iscau3  19236  cmetcaulem  19246  cfilres  19254  bcthlem1  19282  bcthlem5  19286  cncdrg  19318  rlmbn  19320  cniccbdd  19363  ovolunnul  19401  ovolicc  19424  iundisj2  19448  ovolioo  19467  volcn  19503  itg1le  19608  itg2le  19634  iblcnlem  19683  dvfval  19789  dvid  19809  dvcnp2  19811  dvnf  19818  dvnbss  19819  dvn2bss  19821  evlsval2  19946  tdeglem3  19987  mdegldg  19994  mdegmullem  20006  deg1ldgdomn  20022  deg1lt  20025  deg1scl  20041  deg1mul3  20043  q1peqb  20082  fta1b  20097  elplyr  20125  ply1term  20128  dgrub  20158  coe1term  20182  dgradd2  20191  dgrmulc  20194  ofmulrt  20204  quotcl2  20224  quotdgr  20225  facth  20228  quotcan  20231  aannenlem1  20250  aannenlem2  20251  ulmf  20303  ptolemy  20409  tanord1  20444  efif1o  20453  argrege0  20511  logimul  20514  cxpneg  20577  ang180lem1  20656  ang180lem2  20657  ang180lem3  20658  ang180lem4  20659  isosctrlem2  20668  cxp2lim  20820  amgmlem  20833  wilthlem3  20858  sgmppw  20986  lgslem1  21085  lgsneg  21108  lgssq2  21125  lgsdirnn0  21128  lgsqrlem5  21134  lgsquad  21146  dirith  21228  pntrmax  21263  qrngdiv  21323  padicabv  21329  pthistrl  21577  isspthonpth  21589  1pthon  21596  grpoasscan2  21831  grpoinvop  21834  grpopncan  21844  grponpcan  21845  grpopnpcan2  21846  gxneg  21859  gxneg2  21860  gxcom  21862  gxinv  21863  gxsuc  21865  gxadd  21868  gxnn0mul  21870  gxmul  21871  gxmodid  21872  rngoass  21980  rngosn  21997  zerdivemp1  22027  nvpncan2  22142  nvaddsub4  22147  nvnncan  22149  nvdif  22159  nvpi  22160  nvz  22163  nvabs  22167  nv1  22170  imsmetlem  22187  4ipval2  22209  lnoadd  22264  isblo3i  22307  hvsubass  22551  shlub  22921  homco2  23485  leopmul2i  23643  mdslmd4i  23841  atexch  23889  atcvatlem  23893  cdj3lem2  23943  cdj3lem2a  23944  iundisj2f  24035  curry2ima  24102  supxrnemnf  24132  snunioc  24142  ubico  24143  iundisj2fi  24158  divnumden2  24166  xreceu  24173  xdivcl  24175  xdivrec  24178  xrge0addass  24216  ofldaddlt  24246  rhmdvd  24264  redvr  24282  cnre2csqlem  24313  relogbcl  24407  logb1  24408  logblt  24411  hasheuni  24480  sigaclcuni  24506  difelsiga  24521  elsigagen2  24536  sigagenss2  24538  measbase  24556  measval  24557  ismeas  24558  isrnmeas  24559  measxun2  24569  measun  24570  measvunilem  24571  measvuni  24573  mbfmco2  24620  dya2iocnrect  24636  probun  24682  probdif  24683  totprob  24690  probmeasb  24693  cndprobin  24697  cndprobnul  24700  ballotlemfrcn0  24792  erdszelem2  24883  cvmcov2  24967  dedekindle  25193  mulcan1g  25194  subdivcomb1  25200  dfon2lem2  25416  wsuceq123  25570  wzel  25580  frrlem3  25589  brbtwn  25843  brbtwn2  25849  colinearalglem1  25850  colinearalglem2  25851  colinearalg  25854  axcgrid  25860  ax5seglem1  25872  ax5seglem2  25873  axpasch  25885  axlowdimlem16  25901  axcontlem4  25911  axcontlem7  25914  cgrrflx  25926  cgrcomim  25928  cgrtr  25931  cgrtr3  25933  cgrcoml  25935  cgrcomr  25936  cgrtriv  25941  cgrdegen  25943  cgrextend  25947  segconeq  25949  segconeu  25950  btwntriv2  25951  btwntriv1  25955  btwnintr  25958  btwnexch3  25959  btwnouttr2  25961  btwnouttr  25963  btwnexch  25964  funtransport  25970  btwnxfr  25995  colinearex  25999  colineartriv1  26006  colineartriv2  26007  colinearxfr  26014  lineext  26015  linecgr  26020  lineid  26022  idinside  26023  btwnconn1lem7  26032  btwnconn1lem8  26033  btwnconn1lem9  26034  btwnconn1lem12  26037  btwnconn1lem14  26039  btwnconn3  26042  midofsegid  26043  segcon2  26044  seglerflx  26051  segletr  26053  outsidene1  26062  btwnoutside  26064  broutsideof3  26065  outsideoftr  26068  outsideofeq  26069  funray  26079  liness  26084  lineunray  26086  lineelsb2  26087  linecom  26089  linethru  26092  hilbert1.1  26093  bpolycl  26103  bpolydif  26106  areacirclem2  26307  areacirclem5  26310  areacirc  26311  elicc3  26334  clsun  26345  neiin  26349  finlocfin  26393  blbnd  26510  zerdivemp1x  26585  smprngopr  26676  isfldidl  26692  istopclsd  26768  ismrc  26769  mapco2g  26783  mapfzcons  26786  ofmpteq  26790  mzpcl34  26802  mzpexpmpt  26816  mzpsubst  26819  mzpresrename  26821  eldioph  26830  diophrw  26831  eqrabdioph  26850  lerabdioph  26879  ltrabdioph  26882  dvdsrabdioph  26884  diophren  26888  pellex  26912  pell14qrexpclnn0  26943  pellfundex  26963  rmxyadd  26998  rmyabs  27037  jm2.17a  27039  mzpcong  27051  acongeq  27062  coprmdvdsb  27066  modabsdifz  27070  jm2.22  27080  jm2.20nn  27082  rmxdiophlem  27100  rmxdioph  27101  jm3.1  27105  expdiophlem2  27107  islssfgi  27161  pwssplit0  27178  pwssplit1  27179  pwssplit2  27180  pwssplit3  27181  pwssplit4  27182  uvcresum  27233  frlmsplit2  27234  frlmsslss  27235  frlmup4  27244  islindf2  27275  lindsind2  27280  lindff1  27281  f1lindf  27283  lindsss  27285  f1linds  27286  cnsrexpcl  27361  pmtrfrn  27391  idomrootle  27502  fiuneneq  27504  ofdivrec  27534  ofdivcan4  27535  ubelsupr  27681  fnchoice  27690  fmul01  27700  fmuldfeq  27703  fmul01lt1lem2  27705  infrglb  27712  climsuse  27724  stoweidlem16  27755  stoweidlem20  27759  stoweidlem60  27799  wallispilem3  27806  sigaraf  27833  sigarmf  27834  sigaras  27835  sigarms  27836  sigarls  27837  sigarperm  27840  otiunsndisj  28081  otiunsndisjX  28082  leaddsuble  28114  2elfz2melfz  28140  modsubmod  28178  modsubmodmod  28179  modaddmulmod  28181  swrd0fv  28226  cshwidxmod  28277  2cshw1lem1  28282  2cshw2lem1  28286  cshweqdif2  28304  nbfiusgrafi  28328  isrgra  28441  frg2woteu  28518  3orbi123  28668  alrim3con13v  28691  tratrb  28694  3orbi123VD  29036  19.21a3con13vVD  29038  tratrbVD  29047  bnj900  29374  bnj1110  29425  bnj1128  29433  bnj1125  29435  bnj1136  29440  bnj1189  29452  bnj1204  29455  bnj1321  29470  bnj1413  29478  lubunNEW  29845  lfladd  29938  lflsub  29939  lflmul  29940  lkrlsp2  29975  lshpkrlem5  29986  oplecon3b  30072  latm4  30105  omllaw4  30118  omllaw5N  30119  cmtcomlemN  30120  cmtbr2N  30125  cmtbr3N  30126  omlmod1i2N  30132  omlspjN  30133  cvrnbtwn3  30148  cvrcon3b  30149  cvrcmp  30155  cvrcmp2  30156  cvlatexch3  30210  cvlsupr5  30218  cvlsupr7  30220  hlrelat2  30274  2llnneN  30280  cvrval5  30286  cvrexch  30291  cvratlem  30292  atcvr0eq  30297  atcvrneN  30301  atcvrj1  30302  atle  30307  atlt  30308  atlelt  30309  2atjm  30316  3noncolr2  30320  3noncolr1N  30321  hlatcon2  30323  3dim1  30338  3dim2  30339  1cvratex  30344  1cvrat  30347  ps-1  30348  ps-2  30349  2atjlej  30350  hlatexch3N  30351  llnexatN  30392  llncmp  30393  lplni2  30408  lplnnle2at  30412  lplnnleat  30413  lplnri3N  30426  2lplnmN  30430  2llnmj  30431  lplncmp  30433  lplnexatN  30434  2llnm2N  30439  2llnm3N  30440  2llnmeqat  30442  2atnelvolN  30458  4atlem0ae  30465  4atlem0be  30466  4atlem3b  30469  4atlem9  30474  4atlem10a  30475  4atlem10  30477  lvolcmp  30488  2lplnm2N  30492  2lplnmj  30493  pmapglbx  30640  pmapmeet  30644  2llnma1b  30657  2llnma1  30658  2llnma3r  30659  2llnma2  30660  2llnma2rN  30661  elpadd2at  30677  paddasslem16  30706  padd4N  30711  paddclN  30713  pmodlem2  30718  pmapjoin  30723  pmapjat1  30724  pmapjat2  30725  hlmod1i  30727  atmod2i1  30732  atmod2i2  30733  atmod3i1  30735  llnexchb2  30740  dalawlem2  30743  elpcliN  30764  pclssN  30765  pclunN  30769  pclun2N  30770  polcon3N  30788  2polcon4bN  30789  paddunN  30798  poldmj1N  30799  pmapj2N  30800  pmapocjN  30801  psubclinN  30819  paddatclN  30820  poml5N  30825  osumcllem3N  30829  pexmidlem3N  30843  pexmidlem4N  30844  lhple  30913  lhpat4N  30915  4atex2  30948  4atex2-0bOLDN  30950  4atex3  30952  ltrnatb  31008  ltrnel  31010  ltrncnvel  31013  ltrncoelN  31014  ltrncoat  31015  ltrncoval  31016  ltrncnv  31017  ltrn11at  31018  ltrnmw  31022  trlcnv  31036  trljat2  31038  trlat  31040  trl0  31041  ltrnnidn  31045  trlnid  31050  trlval3  31058  trlval4  31059  cdlemc2  31063  cdlemc5  31066  cdlemc6  31067  cdlemd7  31075  cdleme00a  31080  cdleme0e  31088  cdleme01N  31092  cdleme02N  31093  cdleme0ex1N  31094  cdleme0ex2N  31095  cdleme3g  31105  cdleme3h  31106  cdleme3  31108  cdleme4  31109  cdleme5  31111  cdleme7b  31115  cdleme9  31124  cdleme11a  31131  cdleme11dN  31133  cdleme11e  31134  cdleme11g  31136  cdleme11h  31137  cdleme11j  31138  cdleme11k  31139  cdleme12  31142  cdleme18a  31162  cdleme18b  31163  cdleme18c  31164  cdleme22gb  31165  cdleme20zN  31172  cdleme20y  31173  cdleme19a  31174  cdleme20d  31183  cdleme20i  31188  cdleme20j  31189  cdleme20l2  31192  cdleme22a  31211  cdleme22d  31214  cdleme22e  31215  cdleme30a  31249  cdlemefs32sn1aw  31285  cdlemefs29bpre0N  31287  cdlemefs29bpre1N  31288  cdlemefs29cpre1N  31289  cdlemefs29clN  31290  cdleme43fsv1snlem  31291  cdlemefs32fvaN  31293  cdlemefs32fva1  31294  cdlemefs31fv1  31295  cdlemefs45eN  31302  cdleme41sn3a  31304  cdleme32fva  31308  cdleme32fvaw  31310  cdleme32b  31313  cdleme32c  31314  cdleme32e  31316  cdleme35h  31327  cdleme37m  31333  cdleme38m  31334  cdleme40m  31338  cdleme40n  31339  cdleme41sn3aw  31345  cdleme41sn4aw  31346  cdleme41fva11  31348  cdleme42b  31349  cdleme42e  31350  cdleme42h  31353  cdleme42i  31354  cdleme42k  31355  cdleme43cN  31362  cdleme17d2  31366  cdleme17d3  31367  cdleme48fv  31370  cdleme48bw  31373  cdleme48b  31374  cdlemeg47rv2  31381  cdlemeg46c  31384  cdlemeg46sfg  31391  cdlemeg46fjgN  31392  cdlemeg46rjgN  31393  cdlemeg46fjv  31394  cdlemeg46frv  31396  cdlemeg46vrg  31398  cdlemeg46rgv  31399  cdlemeg46req  31400  cdlemeg46gfv  31401  cdlemeg46gfre  31403  cdleme48d  31406  cdlemeg49lebilem  31410  cdleme50trn2  31422  cdleme50ltrn  31428  ltrniotacnvval  31453  ltrniotavalbN  31455  cdlemg1cex  31459  cdlemg2dN  31461  cdlemg2fvlem  31465  cdlemg2fv2  31471  cdlemg2kq  31473  cdlemg2l  31474  cdlemg2m  31475  cdlemg4a  31479  cdlemg4b1  31480  cdlemg4b2  31481  cdlemg4d  31484  cdlemg4e  31485  cdlemg4f  31486  cdlemg4  31488  cdlemg6d  31492  cdlemg6e  31493  cdlemg7fvN  31495  cdlemg8a  31498  cdlemg8b  31499  cdlemg8c  31500  cdlemg9a  31503  cdlemg9b  31504  cdlemg9  31505  cdlemg11aq  31509  cdlemg10c  31510  cdlemg12a  31514  cdlemg12b  31515  cdlemg12c  31516  cdlemg12f  31519  cdlemg12g  31520  cdlemg14f  31524  cdlemg14g  31525  cdlemg17a  31532  cdlemg17dN  31534  cdlemg17e  31536  cdlemg17i  31540  cdlemg17ir  31541  cdlemg17  31548  cdlemg18b  31550  cdlemg18c  31551  cdlemg18d  31552  cdlemg18  31553  cdlemg21  31557  cdlemg28a  31564  cdlemg31b0a  31566  cdlemg31a  31568  cdlemg31b  31569  cdlemg28b  31574  cdlemg33c  31579  cdlemg33d  31580  cdlemg33e  31581  cdlemg35  31584  cdlemg41  31589  ltrnco  31590  trlcocnv  31591  trlcoabs  31592  trlcoabs2N  31593  trlcocnvat  31595  trlconid  31596  trlcolem  31597  trlcone  31599  cdlemg42  31600  cdlemg43  31601  cdlemg44a  31602  cdlemg47a  31605  cdlemg46  31606  trljco  31611  tendoset  31630  tendof  31634  tendoeq1  31635  tendocoval  31637  tendoco2  31639  tendococl  31643  tendoplcl2  31649  tendoplco2  31650  tendopltp  31651  tendoplcl  31652  tendoplcom  31653  cdlemh  31688  cdlemi1  31689  cdlemi2  31690  cdlemk1  31702  cdlemk2  31703  cdlemk3  31704  cdlemk4  31705  cdlemk8  31709  cdlemk9  31710  cdlemk9bN  31711  cdlemki  31712  cdlemkvcl  31713  cdlemk10  31714  cdlemksv2  31718  cdlemk7  31719  cdlemk11  31720  cdlemk12  31721  cdlemk5u  31732  cdlemk6u  31733  cdlemk7u  31741  cdlemk12u  31743  cdlemk22  31764  cdlemk32  31768  cdlemk28-3  31779  cdlemk34  31781  cdlemk29-3  31782  cdlemk39  31787  cdlemkfid1N  31792  cdlemkid1  31793  cdlemkid2  31795  cdlemkfid3N  31796  cdlemk54  31829  cdlemk19u  31841  cdlemk56w  31844  tendoex  31846  cdleml1N  31847  cdleml2N  31848  cdleml3N  31849  cdleml6  31852  cdleml7  31853  cdleml8  31854  cdleml9  31855  tendocnv  31893  tendospcanN  31895  dvhopvadd  31965  tendolinv  31977  tendorinv  31978  dicvaddcl  32062  dicvscacl  32063  cdlemn2  32067  cdlemn2a  32068  cdlemn3  32069  cdlemn4  32070  cdlemn4a  32071  cdlemn5pre  32072  cdlemn6  32074  cdlemn7  32075  cdlemn8  32076  cdlemn9  32077  cdlemn10  32078  cdlemn11a  32079  cdlemn11c  32081  cdlemn11pre  32082  dihordlem6  32085  dihordlem7  32086  dihordlem7b  32087  dihjustlem  32088  dihjust  32089  dihord2cN  32093  dihord11c  32096  dihvalcq2  32119  dihopelvalcpre  32120  dihmeetlem1N  32162  dihglblem3N  32167  dihmeetlem2N  32171  dihglbcpreN  32172  dihmeetcN  32174  dihmeetbclemN  32176  dihmeetlem4preN  32178  dihmeetlem9N  32187  dihmeetlem13N  32191  dihmeetlem20N  32198  dih1dimatlem0  32200  dihlspsnat  32205  dihmeet  32215  dochss  32237  dochdmj1  32262  hdmap1fval  32669  hdmapfval  32702  hgmapfval  32761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator