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  2619  fresaun  5428  foco2  5696  fsnunf  5734  fsnunf2  5735  fnsuppres  5748  fcofo  5814  fveqf1o  5822  f1oiso2  5865  ovmpt2x  5992  ovmpt2ga  5993  ofeq  6096  ofrval  6104  riotass  6349  riotasv2s  6367  onoviun  6376  omwordri  6586  omeulem1  6596  oeord  6602  oewordri  6606  oeordsuc  6608  erov  6771  mapxpen  7043  unbnn  7129  fofinf1o  7153  elfir  7185  dffi2  7192  elfiun  7199  fisup2g  7233  suppr  7235  ordtype2  7265  hartogslem1  7273  wemapso  7282  wemapso2  7283  ixpiunwdom  7321  cnfcom3clem  7424  cdaassen  7824  mapcdaen  7826  infcdaabs  7848  infunabs  7849  infdif  7851  infdif2  7852  cfsmolem  7912  isf32lem11  8005  isf34lem7  8021  zornn0g  8148  ttukey2g  8159  konigthlem  8206  gchdomtri  8267  fpwwe  8284  canthwe  8289  gchaleph  8313  gchaleph2  8314  winainflem  8331  wununi  8344  tsksuc  8400  tskpr  8408  tskop  8409  tskcard  8419  grupw  8433  grurn  8439  gruop  8443  gruun  8444  grumap  8446  gruixp  8447  distrlem4pr  8666  ltadd2  8940  mul31  8996  readdcan  9002  addid2  9011  addsubass  9077  subcan2  9088  subsub2  9091  subsub4  9096  npncan3  9101  pnpcan  9102  pnncan  9104  subcan  9118  subdi  9229  ltadd1  9257  leadd1  9258  leadd2  9259  ltsubadd  9260  lesubadd  9262  lesub1  9284  lesub2  9285  ltsub1  9286  ltsub2  9287  mulcan  9421  mulcan2  9422  divcan2  9448  diveq0  9450  divrec  9456  divrec2  9457  divdir  9463  divcan3  9464  div11  9466  divcan5  9478  redivcl  9495  div2neg  9499  ltmul1  9622  ltdiv1  9636  ltmuldiv  9642  ledivmulOLD  9646  lemuldiv  9651  lt2msq1  9655  suprub  9731  suprlub  9732  infmsup  9748  infmrgelb  9750  infmrlb  9751  ofsubeq0  9759  ofnegsub  9760  ofsubge0  9761  gtndiv  10105  eluz2  10252  peano2uz  10288  suprzub  10325  xrltmin  10527  xrlemin  10529  xaddass  10585  xleadd1  10591  xltadd1  10592  xmulass  10623  xlemul1  10626  xlemul2  10627  xltmul1  10628  xadddi  10631  xadddir  10632  xadddi2  10633  supxrre  10662  infmxrre  10670  ixxssixx  10686  ixxub  10693  ixxlb  10694  lbico1  10722  lbicc2  10768  icoshftf1o  10775  snunioo  10778  snunico  10779  iccsplit  10784  fzrev3  10865  fzm1  10878  fzrevral2  10883  elfzo0  10920  flwordi  10958  flword2  10959  expgt1  11156  exprec  11159  leexp2a  11173  expubnd  11178  sqdiv  11185  expnbnd  11246  expmulnbnd  11249  modexp  11252  bccmpl  11338  ccatass  11452  swrdval  11466  swrdval2  11469  ccatco  11506  s3cl  11543  swrds2  11576  mulre  11622  caubnd  11858  climuni  12042  iseraltlem3  12172  geoisum1c  12352  eflt  12413  rpnnen2lem4  12512  dvdsmultr2  12580  dvdsexp  12600  sadass  12678  dvdsgcdb  12739  gcdass  12740  mulgcd  12741  gcddiv  12744  rplpwr  12751  coprmdvds  12797  mulgcddvds  12799  qredeq  12801  rpexp12i  12817  rpmul  12818  odzcllem  12873  odzphi  12877  pythagtriplem15  12898  pcpremul  12912  pcdiv  12921  pcqmul  12922  pcqdiv  12926  vdwapfval  13034  vdwapun  13037  vdwpc  13043  hashbcss  13067  ramval  13071  0ram2  13084  0ramcl  13086  ramcl  13092  ressbas  13214  xpsadd  13494  xpsmul  13495  mreiincl  13514  mreincl  13517  mrcss  13534  mrcun  13540  submrc  13546  posasymb  14102  meetle  14150  p0le  14165  ple1  14166  latleeqj1  14185  latjlej12  14189  latleeqm1  14201  latmlem12  14205  latnlemlt  14206  latj4  14223  latj4rot  14224  lubss  14241  lubun  14243  clatglbss  14247  pospropd  14254  isipodrs  14280  imasmnd2  14425  gsumccat  14480  frmdup3  14504  grpinvadd  14560  grpsubeq0  14568  grppncan  14572  grpsubpropd2  14583  pwsinvg  14623  imasgrp2  14626  issubg  14637  nsgconj  14666  nsgid  14679  ghmnsgima  14722  odcong  14880  isslw  14935  pgpssslw  14941  lsmsubg  14981  efgsval2  15058  frgpup3  15103  cmn4  15124  ablinvadd  15127  ablsub4  15130  abladdsub4  15131  ablpncan2  15133  lsmsubg2  15167  lsm4  15168  rngcom  15385  imasrng  15418  unitmulcl  15462  unitmulclb  15463  dvrcan1  15489  dvrcan3  15490  irredrmul  15505  isabvd  15601  abvdom  15619  islmod  15647  lmodvsnegOLD  15684  lmodcom  15687  lss0cl  15720  lssvnegcl  15729  lssincl  15738  lspss  15757  lspun  15760  lspsnvsi  15777  lsslsp  15788  lmodvsinv  15809  lmodvsinv2  15810  0lmhm  15813  lsmsp  15855  lsmsp2  15856  lspvadd  15865  lspsntri  15866  lidldvgen  16023  rrgeq0  16047  aspid  16086  aspss  16088  asclmul1  16095  asclmul2  16096  psrbagaddcl  16132  psrbagconcl  16135  coe1tm  16365  coe1sclmul  16374  coe1sclmul2  16376  phllmhm  16552  ip2eq  16573  cssmre  16609  iuncld  16798  clsss  16807  ntrin  16814  clsndisj  16828  iscldtop  16848  neiss  16862  lpss3  16892  restco  16911  restabs  16912  restcldi  16920  restcls  16927  restntr  16928  restlp  16929  lmconst  17007  cnpresti  17032  hausnei2  17097  sshauslem  17116  clscon  17172  concompss  17175  concompclo  17177  kgen2ss  17266  elptr  17284  xkococn  17370  qtopval2  17403  qtoptop2  17406  cmphaushmeo  17507  elmptrab  17538  filinn0  17571  fbasweak  17576  snfbas  17577  filuni  17596  trnei  17603  fmval  17654  rnelfm  17664  flimrest  17694  flimclslem  17695  flfnei  17702  isflf  17704  lmflf  17716  fclsneii  17728  fclsrest  17735  isfcf  17745  ptcmpg  17767  istgp2  17790  divstgpopn  17818  divstgphaus  17821  xmetge0  17925  xmetsym  17928  xmetresbl  17999  mopni3  18056  stdbdxmet  18077  stdbdmopn  18080  prdsxms  18092  prdsms  18093  isngp4  18149  nmsub  18160  nm2dif  18162  nminvr  18196  nmoix  18254  nmods  18269  metds0  18370  metnrm  18382  cncfmptc  18431  iirev  18443  icoopnst  18453  iocopnst  18454  icchmeo  18455  iccpnfhmeo  18459  pi1blem  18553  pi1xfr  18569  isclmi  18591  cphsqrcl  18636  cph2ass  18664  ipcau  18684  nmpar  18686  fmcfil  18714  iscau3  18720  cmetcaulem  18730  cfilres  18738  bcthlem1  18762  bcthlem5  18766  cncdrg  18792  rlmbn  18794  cniccbdd  18837  ovolunnul  18875  ovolicc  18898  iundisj2  18922  ovolioo  18941  volcn  18977  itg1le  19084  itg2le  19110  iblcnlem  19159  dvfval  19263  dvid  19283  dvcnp2  19285  dvnf  19292  dvnbss  19293  dvn2bss  19295  evlsval2  19420  tdeglem3  19461  mdegldg  19468  mdegmullem  19480  deg1ldgdomn  19496  deg1lt  19499  deg1scl  19515  deg1mul3  19517  q1peqb  19556  fta1b  19571  elplyr  19599  ply1term  19602  dgrub  19632  coe1term  19656  dgradd2  19665  dgrmulc  19668  ofmulrt  19678  quotcl2  19698  quotdgr  19699  facth  19702  quotcan  19705  aannenlem1  19724  aannenlem2  19725  ulmf  19777  ptolemy  19880  tanord1  19915  efif1o  19924  argrege0  19981  logimul  19984  cxpneg  20044  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  ang180lem4  20126  isosctrlem2  20135  cxp2lim  20287  amgmlem  20300  wilthlem3  20324  sgmppw  20452  lgslem1  20551  lgsneg  20574  lgssq2  20591  lgsdirnn0  20594  lgsqrlem5  20600  lgsquad  20612  dirith  20694  pntrmax  20729  qrngdiv  20789  padicabv  20795  grpoasscan2  20921  grpoinvop  20924  grpopncan  20934  grponpcan  20935  grpopnpcan2  20936  gxneg  20949  gxneg2  20950  gxcom  20952  gxinv  20953  gxsuc  20955  gxadd  20958  gxnn0mul  20960  gxmul  20961  gxmodid  20962  rngoass  21070  rngosn  21087  nvpncan2  21230  nvaddsub4  21235  nvnncan  21237  nvdif  21247  nvpi  21248  nvz  21251  nvabs  21255  nv1  21258  imsmetlem  21275  4ipval2  21297  lnoadd  21352  isblo3i  21395  hvsubass  21639  shlub  22009  homco2  22573  leopmul2i  22731  mdslmd4i  22929  atexch  22977  atcvatlem  22981  cdj3lem2  23031  cdj3lem2a  23032  ballotlemsgt1  23085  ballotlemfrcn0  23104  xreceu  23121  xdivcl  23123  xdivrec  23126  curry2ima  23262  supxrnemnf  23271  snunioc  23282  ubico  23283  cnre2csqlem  23309  xrge0addass  23344  xrge0adddir  23347  iundisj2fi  23379  iundisj2f  23381  relogbcl  23419  logb1  23420  logblt  23423  hasheuni  23468  sigaclcuni  23494  difelsiga  23509  elsigagen2  23524  measbase  23543  measval  23544  ismeas  23545  isrnmeas  23546  measvun  23552  measxun2  23553  measxun  23554  measvunilem  23555  measvuni  23557  measres  23564  mbfmco2  23585  dya2iocrrnval  23597  probun  23637  probdif  23638  totprob  23645  probmeasb  23648  cndprobin  23652  cndprobtot  23654  cndprobnul  23655  cndprobprob  23656  erdszelem2  23738  cvmcov2  23821  dedekindle  24098  mulcan1g  24099  subdivcomb1  24105  prodmolem2  24158  prodmo  24159  dfon2lem2  24211  frrlem3  24354  brbtwn  24599  brbtwn2  24605  colinearalglem1  24606  colinearalglem2  24607  colinearalg  24610  axcgrid  24616  ax5seglem1  24628  ax5seglem2  24629  axpasch  24641  axlowdimlem16  24657  axcontlem4  24667  axcontlem7  24670  cgrrflx  24682  cgrcomim  24684  cgrtr  24687  cgrtr3  24689  cgrcoml  24691  cgrcomr  24692  cgrtriv  24697  cgrdegen  24699  cgrextend  24703  segconeq  24705  segconeu  24706  btwntriv2  24707  btwntriv1  24711  btwnintr  24714  btwnexch3  24715  btwnouttr2  24717  btwnouttr  24719  btwnexch  24720  funtransport  24726  btwnxfr  24751  colinearex  24755  colineartriv1  24762  colineartriv2  24763  colinearxfr  24770  lineext  24771  linecgr  24776  lineid  24778  idinside  24779  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem12  24793  btwnconn1lem14  24795  btwnconn3  24798  midofsegid  24799  segcon2  24800  seglerflx  24807  segletr  24809  outsidene1  24818  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsideofeq  24825  funray  24835  liness  24840  lineunray  24842  lineelsb2  24843  linecom  24845  linethru  24848  hilbert1.1  24849  bpolycl  24859  bpolydif  24862  areacirclem4  25030  areacirclem6  25033  areacirc  25034  intn3an1d  25039  infxpg  25198  ab2rexex2g  25235  iccleub3  25239  injsurinj  25252  iscst1  25277  jop  25287  cur1vald  25302  preotr2  25338  prltub  25363  ubpar  25364  inposet  25381  dfps2  25392  reacomsmgrp1  25446  reacomsmgrp3  25448  reacomsmgrp4  25449  clfsebs  25450  clfsebsr  25452  fprodadd  25455  abloinvop  25456  mndoio  25461  fprodneg  25481  fprodsub  25482  prsubrtr  25502  multinv  25525  multinvb  25526  fldax3  25533  zerdivemp1  25539  mulveczer  25582  mulinvsca  25583  glmrngo  25585  truni1  25608  npmp  25624  mapdiscn  25630  hmeogrpi  25639  conttnf2  25665  bwt2  25695  mslb1  25710  msra3  25712  limnumrr  25725  lvsovso2  25730  claddrvr  25751  issubrv  25775  ismulcv  25784  clsmulrv  25786  mulmulvec  25790  distmlva  25791  distsava  25792  isdivcv2  25796  divclcvd  25797  divclrvd  25798  imonclem  25916  ismonc  25917  cmpmon  25918  icmpmon  25919  isepic  25927  tartarmap  25991  rocatval  26062  cmp2morpcats  26064  cmp2morpgrp  26066  cmp2morpdom  26067  cmp2morpcod  26068  cmpmorass  26069  indcls2  26099  bisig0  26165  isconcl6a  26206  isib2g1a1  26219  isibg2a1  26222  segline  26244  pxysxy  26245  isibcg  26294  elicc3  26331  clsun  26349  neiin  26353  finlocfin  26402  blbnd  26614  zerdivemp1x  26689  smprngopr  26780  isfldidl  26796  istopclsd  26878  ismrc  26879  mapco2g  26893  mapfzcons  26896  ofmpteq  26900  mzpcl34  26912  mzpexpmpt  26926  mzpsubst  26929  mzpresrename  26931  eldioph  26940  diophrw  26941  eqrabdioph  26960  lerabdioph  26989  ltrabdioph  26992  dvdsrabdioph  26994  diophren  26999  pellex  27023  pell14qrexpclnn0  27054  pellfundex  27074  rmxyadd  27109  rmyabs  27148  jm2.17a  27150  mzpcong  27162  acongeq  27173  coprmdvdsb  27177  modabsdifz  27181  jm2.22  27191  jm2.20nn  27193  rmxdiophlem  27211  rmxdioph  27212  jm3.1  27216  expdiophlem2  27218  islssfgi  27273  pwssplit0  27290  pwssplit1  27291  pwssplit2  27292  pwssplit3  27293  pwssplit4  27294  uvcresum  27345  frlmsplit2  27346  frlmsslss  27347  frlmup4  27356  islindf2  27387  lindsind2  27392  lindff1  27393  f1lindf  27395  lindsss  27397  f1linds  27398  cnsrexpcl  27473  pmtrfrn  27503  idomrootle  27614  fiuneneq  27616  ofdivrec  27646  ofdivcan4  27647  ubelsupr  27794  fnchoice  27803  fmul01  27813  fmuldfeq  27816  fmul01lt1lem2  27818  infrglb  27825  climsuse  27837  ibliccsinexp  27848  stoweidlem16  27868  stoweidlem20  27872  stoweidlem22  27874  stoweidlem26  27878  stoweidlem31  27883  stoweidlem34  27886  stoweidlem43  27895  stoweidlem44  27896  stoweidlem51  27903  stoweidlem52  27904  stoweidlem57  27909  stoweidlem60  27912  wallispilem3  27919  sigaraf  27946  sigarmf  27947  sigaras  27948  sigarms  27949  sigarls  27950  sigarperm  27953  pthistrl  28358  3orbi123  28572  alrim3con13v  28595  tratrb  28598  3orbi123VD  28942  19.21a3con13vVD  28944  tratrbVD  28953  bnj900  29277  bnj1110  29328  bnj1128  29336  bnj1125  29338  bnj1136  29343  bnj1189  29355  bnj1204  29358  bnj1321  29373  bnj1413  29381  lubunNEW  29785  lfladd  29878  lflsub  29879  lflmul  29880  lkrlsp2  29915  lshpkrlem5  29926  oplecon3b  30012  latm4  30045  omllaw4  30058  omllaw5N  30059  cmtcomlemN  30060  cmtbr2N  30065  cmtbr3N  30066  omlmod1i2N  30072  omlspjN  30073  cvrnbtwn3  30088  cvrcon3b  30089  cvrcmp  30095  cvrcmp2  30096  cvlatexch3  30150  cvlsupr5  30158  cvlsupr7  30160  hlrelat2  30214  2llnneN  30220  cvrval5  30226  cvrexch  30231  cvratlem  30232  atcvr0eq  30237  atcvrneN  30241  atcvrj1  30242  atle  30247  atlt  30248  atlelt  30249  2atjm  30256  3noncolr2  30260  3noncolr1N  30261  hlatcon2  30263  3dim1  30278  3dim2  30279  1cvratex  30284  1cvrat  30287  ps-1  30288  ps-2  30289  2atjlej  30290  hlatexch3N  30291  llnexatN  30332  llncmp  30333  lplni2  30348  lplnnle2at  30352  lplnnleat  30353  lplnri3N  30366  2lplnmN  30370  2llnmj  30371  lplncmp  30373  lplnexatN  30374  2llnm2N  30379  2llnm3N  30380  2llnmeqat  30382  2atnelvolN  30398  4atlem0ae  30405  4atlem0be  30406  4atlem3b  30409  4atlem9  30414  4atlem10a  30415  4atlem10  30417  lvolcmp  30428  2lplnm2N  30432  2lplnmj  30433  pmapglbx  30580  pmapmeet  30584  2llnma1b  30597  2llnma1  30598  2llnma3r  30599  2llnma2  30600  2llnma2rN  30601  elpadd2at  30617  paddasslem16  30646  padd4N  30651  paddclN  30653  pmodlem2  30658  pmapjoin  30663  pmapjat1  30664  pmapjat2  30665  hlmod1i  30667  atmod2i1  30672  atmod2i2  30673  atmod3i1  30675  llnexchb2  30680  dalawlem2  30683  elpcliN  30704  pclssN  30705  pclunN  30709  pclun2N  30710  polcon3N  30728  2polcon4bN  30729  paddunN  30738  poldmj1N  30739  pmapj2N  30740  pmapocjN  30741  psubclinN  30759  paddatclN  30760  poml5N  30765  osumcllem3N  30769  pexmidlem3N  30783  pexmidlem4N  30784  lhple  30853  lhpat4N  30855  4atex2  30888  4atex2-0bOLDN  30890  4atex3  30892  ltrnatb  30948  ltrnel  30950  ltrncnvel  30953  ltrncoelN  30954  ltrncoat  30955  ltrncoval  30956  ltrncnv  30957  ltrn11at  30958  ltrnmw  30962  trlcnv  30976  trljat2  30978  trlat  30980  trl0  30981  ltrnnidn  30985  trlnid  30990  trlval3  30998  trlval4  30999  cdlemc2  31003  cdlemc5  31006  cdlemc6  31007  cdlemd7  31015  cdleme00a  31020  cdleme0e  31028  cdleme01N  31032  cdleme02N  31033  cdleme0ex1N  31034  cdleme0ex2N  31035  cdleme3g  31045  cdleme3h  31046  cdleme3  31048  cdleme4  31049  cdleme5  31051  cdleme7b  31055  cdleme9  31064  cdleme11a  31071  cdleme11dN  31073  cdleme11e  31074  cdleme11g  31076  cdleme11h  31077  cdleme11j  31078  cdleme11k  31079  cdleme12  31082  cdleme18a  31102  cdleme18b  31103  cdleme18c  31104  cdleme22gb  31105  cdleme20zN  31112  cdleme20y  31113  cdleme19a  31114  cdleme20d  31123  cdleme20i  31128  cdleme20j  31129  cdleme20l2  31132  cdleme22a  31151  cdleme22d  31154  cdleme22e  31155  cdleme30a  31189  cdlemefs32sn1aw  31225  cdlemefs29bpre0N  31227  cdlemefs29bpre1N  31228  cdlemefs29cpre1N  31229  cdlemefs29clN  31230  cdleme43fsv1snlem  31231  cdlemefs32fvaN  31233  cdlemefs32fva1  31234  cdlemefs31fv1  31235  cdlemefs45eN  31242  cdleme41sn3a  31244  cdleme32fva  31248  cdleme32fvaw  31250  cdleme32b  31253  cdleme32c  31254  cdleme32e  31256  cdleme35h  31267  cdleme37m  31273  cdleme38m  31274  cdleme40m  31278  cdleme40n  31279  cdleme41sn3aw  31285  cdleme41sn4aw  31286  cdleme41fva11  31288  cdleme42b  31289  cdleme42e  31290  cdleme42h  31293  cdleme42i  31294  cdleme42k  31295  cdleme43cN  31302  cdleme17d2  31306  cdleme17d3  31307  cdleme48fv  31310  cdleme48bw  31313  cdleme48b  31314  cdlemeg47rv2  31321  cdlemeg46c  31324  cdlemeg46sfg  31331  cdlemeg46fjgN  31332  cdlemeg46rjgN  31333  cdlemeg46fjv  31334  cdlemeg46frv  31336  cdlemeg46vrg  31338  cdlemeg46rgv  31339  cdlemeg46req  31340  cdlemeg46gfv  31341  cdlemeg46gfre  31343  cdleme48d  31346  cdlemeg49lebilem  31350  cdleme50trn2  31362  cdleme50ltrn  31368  ltrniotacnvval  31393  ltrniotavalbN  31395  cdlemg1cex  31399  cdlemg2dN  31401  cdlemg2fvlem  31405  cdlemg2fv2  31411  cdlemg2kq  31413  cdlemg2l  31414  cdlemg2m  31415  cdlemg4a  31419  cdlemg4b1  31420  cdlemg4b2  31421  cdlemg4d  31424  cdlemg4e  31425  cdlemg4f  31426  cdlemg4  31428  cdlemg6d  31432  cdlemg6e  31433  cdlemg7fvN  31435  cdlemg8a  31438  cdlemg8b  31439  cdlemg8c  31440  cdlemg9a  31443  cdlemg9b  31444  cdlemg9  31445  cdlemg11aq  31449  cdlemg10c  31450  cdlemg12a  31454  cdlemg12b  31455  cdlemg12c  31456  cdlemg12f  31459  cdlemg12g  31460  cdlemg14f  31464  cdlemg14g  31465  cdlemg17a  31472  cdlemg17dN  31474  cdlemg17e  31476  cdlemg17i  31480  cdlemg17ir  31481  cdlemg17  31488  cdlemg18b  31490  cdlemg18c  31491  cdlemg18d  31492  cdlemg18  31493  cdlemg21  31497  cdlemg28a  31504  cdlemg31b0a  31506  cdlemg31a  31508  cdlemg31b  31509  cdlemg28b  31514  cdlemg33c  31519  cdlemg33d  31520  cdlemg33e  31521  cdlemg35  31524  cdlemg41  31529  ltrnco  31530  trlcocnv  31531  trlcoabs  31532  trlcoabs2N  31533  trlcocnvat  31535  trlconid  31536  trlcolem  31537  trlcone  31539  cdlemg42  31540  cdlemg43  31541  cdlemg44a  31542  cdlemg47a  31545  cdlemg46  31546  trljco  31551  tendoset  31570  tendof  31574  tendoeq1  31575  tendocoval  31577  tendoco2  31579  tendococl  31583  tendoplcl2  31589  tendoplco2  31590  tendopltp  31591  tendoplcl  31592  tendoplcom  31593  cdlemh  31628  cdlemi1  31629  cdlemi2  31630  cdlemk1  31642  cdlemk2  31643  cdlemk3  31644  cdlemk4  31645  cdlemk8  31649  cdlemk9  31650  cdlemk9bN  31651  cdlemki  31652  cdlemkvcl  31653  cdlemk10  31654  cdlemksv2  31658  cdlemk7  31659  cdlemk11  31660  cdlemk12  31661  cdlemk5u  31672  cdlemk6u  31673  cdlemk7u  31681  cdlemk12u  31683  cdlemk22  31704  cdlemk32  31708  cdlemk28-3  31719  cdlemk34  31721  cdlemk29-3  31722  cdlemk39  31727  cdlemkfid1N  31732  cdlemkid1  31733  cdlemkid2  31735  cdlemkfid3N  31736  cdlemk54  31769  cdlemk19u  31781  cdlemk56w  31784  tendoex  31786  cdleml1N  31787  cdleml2N  31788  cdleml3N  31789  cdleml6  31792  cdleml7  31793  cdleml8  31794  cdleml9  31795  tendocnv  31833  tendospcanN  31835  dvhopvadd  31905  tendolinv  31917  tendorinv  31918  dicvaddcl  32002  dicvscacl  32003  cdlemn2  32007  cdlemn2a  32008  cdlemn3  32009  cdlemn4  32010  cdlemn4a  32011  cdlemn5pre  32012  cdlemn6  32014  cdlemn7  32015  cdlemn8  32016  cdlemn9  32017  cdlemn10  32018  cdlemn11a  32019  cdlemn11c  32021  cdlemn11pre  32022  dihordlem6  32025  dihordlem7  32026  dihordlem7b  32027  dihjustlem  32028  dihjust  32029  dihord2cN  32033  dihord11c  32036  dihvalcq2  32059  dihopelvalcpre  32060  dihmeetlem1N  32102  dihglblem3N  32107  dihmeetlem2N  32111  dihglbcpreN  32112  dihmeetcN  32114  dihmeetbclemN  32116  dihmeetlem4preN  32118  dihmeetlem9N  32127  dihmeetlem13N  32131  dihmeetlem20N  32138  dih1dimatlem0  32140  dihlspsnat  32145  dihmeet  32155  dochss  32177  dochdmj1  32202  hdmap1fval  32609  hdmapfval  32642  hgmapfval  32701
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