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

Theorem simp1l 1020
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1l

Proof of Theorem simp1l
StepHypRef Expression
1 simpl 457 . 2
213ad2ant1 1017 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpl1l  1047  simpr1l  1053  simp11l  1107  simp21l  1113  simp31l  1119  funprg  5642  tfisi  6693  omeulem2  7251  uniinqs  7410  unxpdomlem3  7746  elfiun  7910  cantnffval  8101  tcrank  8323  cofsmo  8670  isfin2-2  8720  tskint  9184  tskun  9185  tskurn  9188  gruina  9217  dedekind  9765  dmdcan  10279  lt2msq1  10453  supmullem1  10534  supmul  10536  xaddass  11470  xaddass2  11471  xlt2add  11481  xmulasslem3  11507  xadddi2r  11519  iccsplit  11682  expaddzlem  12209  expaddz  12210  expmulz  12212  ccatopth2  12696  swrdccat3  12717  resqrtcl  13087  limsupgle  13300  o1add  13436  o1mul  13437  o1sub  13438  bitsfzo  14085  sadfval  14102  smufval  14127  prmexpb  14258  4sqlem18  14480  vdwlem10  14508  fsets  14658  submre  15002  mrelatlub  15816  mndodcong  16566  subgabl  16844  gex2abl  16857  cntzsubr  17461  abvres  17488  lbsind2  17727  lspsneu  17769  lbsextlem2  17805  lbsextg  17808  lindfind2  18853  matring  18945  maducoeval  19141  maducoeval2  19142  maduf  19143  madurid  19146  gsummatr01  19161  cramerimplem3  19187  cnprest  19790  hausnei2  19854  isreg2  19878  cmpcld  19902  llyrest  19986  nllyrest  19987  csdfil  20395  hausflimlem  20480  ssblps  20925  ssbl  20926  dvres2  22316  plyadd  22614  plymul  22615  coeeu  22622  vieta1  22708  aalioulem3  22730  aalioulem4  22731  efgh  22928  cxpadd  23060  cxpsub  23063  mulcxp  23066  divcxp  23068  cxple2  23078  cxplt2  23079  cxpcn3lem  23121  angcan  23134  ang180lem5  23145  isosctrlem3  23154  logexprlim  23500  abvcxp  23800  padicabv  23815  brbtwn2  24208  ax5seglem6  24237  axcontlem4  24270  axcontlem8  24274  clwwlknimp  24776  chscllem4  26558  ogrpinvlt  27714  poseq  29333  wsuclem  29381  nofulllem5  29466  ifscgr  29694  congtr  30903  fzmaxdif  30919  isnumbasgrplem2  31053  mullimc  31622  mullimcf  31629  islpcn  31645  cncfuni  31689  icccncfext  31690  stoweidlem34  31816  stoweidlem59  31841  stirlinglem13  31868  fourierdlem41  31930  fourierdlem42  31931  fourierdlem73  31962  lincscm  33031  lincext3  33057  el0ldep  33067  el0ldepsnzr  33068  lshpnelb  34709  lfl1  34795  lshpkrlem6  34840  lshpkrex  34843  hlrelat3  35136  atbtwnexOLDN  35171  atbtwnex  35172  3dim3  35193  3atlem5  35211  2llnmat  35248  lvolex3N  35262  lvolnle3at  35306  4atlem11  35333  4atlem12  35336  dalemccea  35407  cdlema2N  35516  paddasslem2  35545  atmod1i1m  35582  lhp2lt  35725  lhp0lt  35727  lhpj1  35746  lhpmcvr4N  35750  lhpelim  35761  lhpmod2i2  35762  lhpmod6i1  35763  cdlemb2  35765  lhple  35766  lhpat  35767  4atex  35800  4atex2-0aOLDN  35802  4atex3  35805  ldilco  35840  ltrncl  35849  ltrn11  35850  ltrnle  35853  ltrncnvleN  35854  ltrnm  35855  ltrnj  35856  ltrncvr  35857  ltrnatb  35861  ltrnel  35863  ltrncnvel  35866  ltrncnv  35870  ltrnmwOLD  35876  trlval2  35888  trlcnv  35890  trljat1  35891  trljat2  35892  trl0  35895  ltrnnidn  35899  trlnidatb  35902  cdlemc1  35916  cdlemc2  35917  cdlemc5  35920  cdlemc6  35921  cdlemd3  35925  cdlemd6  35928  cdleme0aa  35935  cdleme0b  35937  cdleme0c  35938  cdleme0e  35942  cdleme0fN  35943  cdleme01N  35946  cdleme02N  35947  cdleme0ex1N  35948  cdleme0moN  35950  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme4  35963  cdleme4a  35964  cdleme5  35965  cdleme8  35975  cdleme9  35978  cdleme10  35979  cdleme16aN  35984  cdleme11a  35985  cdleme11fN  35989  cdleme11g  35990  cdleme11h  35991  cdleme11j  35992  cdleme11k  35993  cdleme12  35996  cdleme13  35997  cdleme17c  36013  cdleme17d1  36014  cdleme18a  36016  cdleme18b  36017  cdleme18c  36018  cdleme22gb  36019  cdlemeda  36023  cdlemednpq  36024  cdlemednuN  36025  cdleme19c  36031  cdleme20aN  36035  cdleme20bN  36036  cdleme20c  36037  cdleme22aa  36065  cdleme22a  36066  cdleme22b  36067  cdleme22d  36069  cdleme22e  36070  cdleme27cl  36092  cdleme27a  36093  cdleme30a  36104  cdleme42a  36197  cdleme42c  36198  cdleme50laut  36273  cdlemf1  36287  cdlemf  36289  cdlemfnid  36290  trlord  36295  cdlemg2fv2  36326  cdlemg2kq  36328  cdlemg2m  36330  cdlemg4a  36334  cdlemg4d  36339  cdlemg4g  36342  cdlemg4  36343  cdlemg6c  36346  cdlemg7aN  36351  cdlemg8a  36353  cdlemg8b  36354  cdlemg8c  36355  cdlemg9a  36358  cdlemg9b  36359  cdlemg9  36360  cdlemg11aq  36364  cdlemg10c  36365  cdlemg12a  36369  cdlemg12b  36370  cdlemg12c  36371  cdlemg17a  36387  cdlemg18b  36405  cdlemg18c  36406  cdlemg31b0a  36421  cdlemg31a  36423  cdlemg31b  36424  cdlemg31d  36426  cdlemg35  36439  trlcoabs2N  36448  trlcolem  36452  cdlemg44a  36457  trljco  36466  trljco2  36467  tendoco2  36494  tendopltp  36506  cdlemi1  36544  cdlemi2  36545  cdlemj3  36549  tendocan  36550  cdlemk3  36559  cdlemk4  36560  cdlemk5a  36561  cdlemk9  36565  cdlemk9bN  36566  cdlemkvcl  36568  cdlemk10  36569  cdlemk30  36620  cdlemk31  36622  cdlemk39  36642  cdlemkfid1N  36647  cdlemkid1  36648  cdlemkid2  36650  cdlemkfid3N  36651  cdlemk19ylem  36656  cdlemk19xlem  36668  cdlemk19x  36669  cdlemk53b  36682  cdlemk53  36683  cdlemk54  36684  cdlemk55a  36685  cdlemk43N  36689  cdlemk19u1  36695  cdlemk19u  36696  cdleml1N  36702  erngdvlem4  36717  erngdvlem4-rN  36725  dia11N  36775  cdlemm10N  36845  dib11N  36887  cdlemn2  36922  cdlemn10  36933  dihjustlem  36943  dihord2cN  36948  dihlsscpre  36961  dih1dimb2  36968  dihvalcq2  36974  dihopelvalcpre  36975  dihord6b  36987  dih11  36992  dihmeetlem1N  37017  dihglblem2N  37021  dihglblem3N  37022  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetcN  37029  dihmeetbclemN  37031  dihmeetlem4preN  37033  dihmeetlem9N  37042  dihmeetlem20N  37053  dihlspsnssN  37059  dihlspsnat  37060  dihatlat  37061  dihglblem6  37067  dihmeet  37070  dochss  37092  hdmapval3N  37568  hgmap11  37632
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator