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

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

Proof of Theorem simp2l
StepHypRef Expression
1 simpl 457 . 2
213ad2ant2 1018 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpl2l  1049  simpr2l  1055  simp12l  1109  simp22l  1115  simp32l  1121  funprg  5642  fsnunf  6109  f1oiso2  6248  omeulem2  7251  uniinqs  7410  unxpdomlem3  7746  gruina  9217  dedekind  9765  addid2  9784  dmdcan  10279  xaddass  11470  xaddass2  11471  xlt2add  11481  xmulasslem3  11507  xadddi2  11518  xadddi2r  11519  expaddzlem  12209  expaddz  12210  expmulz  12212  expdiv  12216  modexp  12301  ccatopth2  12696  swrdco  12803  o1add  13436  o1mul  13437  o1sub  13438  ntrivcvgmul  13711  prmexpb  14258  pcpremul  14367  pcdiv  14376  pcqmul  14377  pcqdiv  14381  4sqlem12  14474  f1ocpbllem  14921  ercpbl  14946  erlecpbl  14947  latjlej12  15697  latmlem12  15713  latj4  15731  latj4rot  15732  symgsssg  16492  symgfisg  16493  mndodcong  16566  cmn4  16817  ablsub4  16823  abladdsub4  16824  lsm4  16866  abvdom  17487  abvres  17488  abvtrivd  17489  lspsnvs  17760  lspsneu  17769  lspfixed  17774  lspexch  17775  lsmcv  17787  lspsolvlem  17788  coe1sclmulfv  18324  matvscacell  18938  m1detdiag  19099  cramerimplem3  19187  cnprest  19790  hausnei2  19854  isreg2  19878  cmpcld  19902  llyrest  19986  nllyrest  19987  elptr  20074  basqtop  20212  hausflimlem  20480  tmdgsum  20594  utop2nei  20753  trcfilu  20797  ssblps  20925  ssbl  20926  prdsxmslem2  21032  tgqioo  21305  metnrm  21366  bndth  21458  cph2ass  21659  lmmbr2  21698  iscau3  21717  bcthlem5  21767  ovolunlem2  21909  dvres2  22316  dvfsumlem2  22428  plyadd  22614  plymul  22615  coeeu  22622  coemullem  22647  aalioulem4  22731  mulcxp  23066  cxplea  23077  cxple2  23078  cxplt2  23079  cxpcn3lem  23121  angcan  23134  ang180lem5  23145  divsqrtsumlem  23309  logexprlim  23500  dchrvmasumlema  23685  dchrisum0lema  23699  logdivsum  23718  log2sumbnd  23729  abvcxp  23800  padicabv  23815  tghilbert1_2  24018  brbtwn2  24208  axcontlem4  24270  axcontlem8  24274  1pthon  24593  clwwlkel  24793  gxmodid  25281  chscllem4  26558  orngmul  27793  measxun2  28181  measun  28182  mbfmco2  28236  probun  28358  nofulllem5  29466  cgrcomim  29639  cgrcoml  29646  cgrcomr  29647  cgrdegen  29654  btwnintr  29669  btwnexch3  29670  btwnouttr2  29672  btwnouttr  29674  btwnexch  29675  btwndiff  29677  lineid  29733  idinside  29734  btwnconn1lem7  29743  btwnconn1lem8  29744  btwnconn1lem9  29745  btwnconn1lem12  29748  btwnconn1lem14  29750  btwnconn3  29753  midofsegid  29754  segcon2  29755  brsegle2  29759  btwnoutside  29775  outsideoftr  29779  outsideofeu  29781  linethru  29803  cnres2  30259  heibor  30317  mzpsubst  30681  pellexlem5  30769  pellex  30771  pell14qrexpclnn0  30802  pellfundex  30822  qirropth  30844  monotuz  30877  expmordi  30883  congtr  30903  congmul  30905  congsub  30908  mzpcong  30910  fzmaxdif  30919  jm2.15nn0  30945  idomsubgmo  31155  fourierdlem42  31931  fourierdlem48  31937  fourierdlem80  31969  lidldomn1  32727  rngccatidOLD  32797  coe1sclmulval  32985  lincdifsn  33025  lsmsat  34733  lkrlsp  34827  lkrlsp2  34828  lkrlsp3  34829  latm4  34958  omlspjN  34986  hlatj4  35098  4noncolr3  35177  4noncolr2  35178  4noncolr1  35179  athgt  35180  3dimlem3a  35184  3dimlem4a  35187  3dimlem4  35188  3dimlem4OLDN  35189  3dim3  35193  1cvratex  35197  hlatexch4  35205  3atlem4  35210  atcvrlln2  35243  atcvrlln  35244  lplnnlelln  35267  lvoli2  35305  lvolnlelln  35308  lvolnlelpln  35309  4atlem11b  35332  4atlem12b  35335  2lplnja  35343  2lplnj  35344  dalemyeo  35356  dath2  35461  lncvrat  35506  cdlemblem  35517  cdlemb  35518  elpaddri  35526  padd4N  35564  llnmod2i2  35587  llnexchb2  35593  dalawlem1  35595  dalawlem2  35596  pclfinN  35624  osumcllem6N  35685  pexmidlem3N  35696  lhp2lt  35725  lhp2at0  35756  lhp2atnle  35757  lhp2atne  35758  lhp2at0nle  35759  lhp2at0ne  35760  lhpelim  35761  lhpmod2i2  35762  lhpmod6i1  35763  lhple  35766  lhpat  35767  lhpat3  35770  ltrncoelN  35867  ltrncoat  35868  ltrncnv  35870  trlat  35894  trl0  35895  ltrnnidn  35899  trlnid  35904  cdlemd7  35929  cdleme0b  35937  cdleme0c  35938  cdleme0fN  35943  cdleme02N  35947  cdleme0ex1N  35948  cdleme0ex2N  35949  cdleme7aa  35967  cdleme7c  35970  cdleme7d  35971  cdleme7e  35972  cdleme7ga  35973  cdleme7  35974  cdleme8  35975  cdleme11a  35985  cdleme17c  36013  cdleme22gb  36019  cdlemeda  36023  cdleme20k  36045  cdleme21a  36051  cdleme21d  36056  cdleme22f2  36073  cdleme22g  36074  cdleme23a  36075  cdleme23b  36076  cdleme23c  36077  cdleme24  36078  cdleme28  36099  cdlemefrs32fva1  36127  cdlemefr32sn2aw  36130  cdlemefs32sn1aw  36140  cdleme41sn3a  36159  cdleme32fva  36163  cdleme32fva1  36164  cdleme35a  36174  cdleme35b  36176  cdleme35c  36177  cdleme35f  36180  cdleme39a  36191  cdleme42a  36197  cdleme42c  36198  cdleme42b  36204  cdleme42e  36205  cdleme42f  36206  cdleme42g  36207  cdleme42h  36208  cdleme43bN  36216  cdleme46f2g2  36219  cdleme17d2  36221  cdleme17d4  36223  cdleme48fv  36225  cdleme48fvg  36226  cdleme4gfv  36233  cdlemeg46c  36239  cdlemeg46nlpq  36243  cdlemeg46gfre  36258  cdleme48d  36261  cdlemeg49lebilem  36265  cdleme50trn2  36277  cdleme50ltrn  36283  cdleme  36286  cdlemf1  36287  cdlemf  36289  trlord  36295  ltrniotacnvval  36308  ltrniotavalbN  36310  cdlemg1cex  36314  cdlemg2dN  36316  cdlemg2ce  36318  cdlemg2fvlem  36320  cdlemg2idN  36322  cdlemg2kq  36328  cdlemg2l  36329  cdlemg2m  36330  cdlemg4b2  36336  cdlemg7fvN  36350  cdlemg8a  36353  cdlemg10bALTN  36362  cdlemg11aq  36364  cdlemg12d  36372  cdlemg13a  36377  cdlemg13  36378  cdlemg14f  36379  cdlemg14g  36380  cdlemg17a  36387  cdlemg17b  36388  cdlemg27a  36418  cdlemg31b0N  36420  cdlemg31a  36423  cdlemg31b  36424  cdlemg31c  36425  ltrnco  36445  trlcoabs  36447  trlcoabs2N  36448  trlcocnvat  36450  trlconid  36451  trlcolem  36452  trlcone  36454  cdlemg42  36455  cdlemg43  36456  cdlemg46  36461  cdlemg47  36462  tendoeq1  36490  tendoco2  36494  tendoplco2  36505  tendopltp  36506  cdlemh1  36541  cdlemh2  36542  cdlemi1  36544  cdlemi  36546  cdlemk1  36557  cdlemk2  36558  cdlemk3  36559  cdlemk4  36560  cdlemk8  36564  cdlemk9  36565  cdlemk9bN  36566  cdlemk31  36622  cdlemk32  36623  cdlemk28-3  36634  cdlemk19u  36696  cdlemk56w  36699  tendoex  36701  erngdvlem4  36717  erngdvlem4-rN  36725  dia11N  36775  dib11N  36887  cdlemn6  36929  cdlemn7  36930  cdlemn8  36931  cdlemn9  36932  dihordlem6  36940  dihordlem7  36941  dihord1  36945  dihord2a  36946  dihord2b  36947  dihord2pre  36952  dihord2pre2  36953  dihlsscpre  36961  dihvalcq2  36974  dihopelvalcpre  36975  dihord4  36985  dihord6b  36987  dihmeetlem1N  37017  dihglblem3N  37022  dihmeetlem2N  37026  dihglbcpreN  37027  dihmeetcN  37029  dihmeetbclemN  37031  dihmeetlem4preN  37033  dihjatc1  37038  dihjatc2N  37039  dihjatc3  37040  dihmeetlem9N  37042  dihmeetlem13N  37046  dihmeetlem20N  37053  dih1dimatlem0  37055  mapdpglem24  37431  mapdpglem32  37432  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  mapdh9aOLDN  37518  hdmap14lem6  37603
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