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

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

Proof of Theorem simp3l
StepHypRef Expression
1 simpl 457 . 2
213ad2ant3 1019 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpl3l  1051  simpr3l  1057  simp13l  1111  simp23l  1117  simp33l  1123  disjss3  4451  tfisi  6693  tfrlem5  7068  omeulem1  7250  omeulem2  7251  uniinqs  7410  elfiun  7910  tcrank  8323  isfin2-2  8720  konigthlem  8964  gruen  9211  addid2  9784  mulcan  10211  mulcan2  10212  divass  10250  divdir  10255  div11  10258  divcan5  10271  ltmul1  10417  ltdiv1  10431  ltmuldiv  10440  lediv2  10460  xaddass2  11471  xlt2add  11481  xmulasslem3  11507  xadddi2  11518  expaddz  12210  expmulz  12212  resqrtcl  13087  o1add  13436  o1mul  13437  o1sub  13438  dvdsadd2b  14028  dvdsgcd  14181  rpexp12i  14263  pythagtriplem3  14342  pcpremul  14367  pceu  14370  pcqmul  14377  pcqdiv  14381  f1ocpbllem  14921  funcoppc  15244  funcres  15265  catcisolem  15433  1stfcl  15466  2ndfcl  15467  prfcl  15472  evlfcl  15491  curf1cl  15497  curfcl  15501  hofcl  15528  latjlej12  15697  latmlem12  15713  latj4  15731  latj4rot  15732  symgsssg  16492  symgfisg  16493  psgnunilem4  16522  odcong  16573  cmn4  16817  ablsub4  16823  abladdsub4  16824  lsm4  16866  abvdom  17487  abvres  17488  abvtrivd  17489  lspsolvlem  17788  lbsextlem2  17805  lidlsubcl  17863  frlmbas3  18807  matmulcell  18947  marrepeval  19065  ma1repveval  19073  submaeval  19084  mdetunilem3  19116  mdetuni0  19123  mdetmul  19125  minmar1eval  19151  nllyrest  19987  hausflimlem  20480  tsmsxp  20657  psmetlecl  20819  xmetlecl  20849  prdsxmetlem  20871  bndth  21458  cph2ass  21659  iscau3  21717  dvres2  22316  coemullem  22647  vieta1  22708  aalioulem4  22731  cxpcn3lem  23121  angcan  23134  dchrvmasumlema  23685  logdivsum  23718  abvcxp  23800  padicabv  23815  ax5seglem3  24234  ax5seglem6  24237  axpasch  24244  axeuclid  24266  axcontlem4  24270  axcontlem8  24274  clwwlknimp  24776  gxneg  25268  gxsuc  25274  gxmodid  25281  adjlnop  27005  xreceu  27618  orngmul  27793  rhmdvd  27811  measvunilem  28183  measvunilem0  28184  measres  28193  subdivcomb1  29105  subdivcomb2  29106  cgrcomim  29639  cgrcoml  29646  cgrcomr  29647  cgrdegen  29654  segconeu  29661  btwnintr  29669  btwnexch3  29670  btwnouttr2  29672  btwnouttr  29674  btwnexch  29675  trisegint  29678  lineext  29726  linecgr  29731  lineid  29733  idinside  29734  btwnconn1lem3  29739  btwnconn1lem4  29740  btwnconn1lem7  29743  btwnconn1lem14  29750  btwnconn2  29752  midofsegid  29754  btwnoutside  29775  outsideoftr  29779  lineunray  29797  lineelsb2  29798  cnres2  30259  heibor  30317  mzpsubst  30681  pellex  30771  pellfundex  30822  pellfund14gap  30823  qirropth  30844  rmxypos  30885  congmul  30905  congsub  30908  mzpcong  30910  coprmdvdsb  30925  jm2.15nn0  30945  jm2.16nn0  30946  rpnnen3lem  30973  idomsubgmo  31155  mullimc  31622  islptre  31625  limccog  31626  mullimcf  31629  addlimc  31654  0ellimcdiv  31655  stoweidlem57  31839  fourierdlem48  31937  fourierdlem80  31969  fourierdlem113  32002  bnj1128  34046  lsmcv2  34754  lcvat  34755  lcvexchlem4  34762  lcvexchlem5  34763  lfladd  34791  lflsub  34792  lflmul  34793  lshpkrlem4  34838  latm4  34958  omlmod1i2N  34985  cvlatexch3  35063  cvlsupr7  35073  hlatj4  35098  hlrelat3  35136  cvrval3  35137  atcvrj1  35155  atlelt  35162  2atlt  35163  2atjm  35169  3noncolr2  35173  athgt  35180  3dimlem2  35183  3dimlem4  35188  3dimlem4OLDN  35189  3dim3  35193  1cvratex  35197  ps-1  35201  ps-2  35202  hlatexch3N  35204  llnle  35242  atcvrlln2  35243  atcvrlln  35244  lplni2  35261  lplnle  35264  lplnnle2at  35265  llncvrlpln2  35281  lplnexllnN  35288  2llnmeqat  35295  lvolnle3at  35306  4atlem0ae  35318  lplncvrlvol2  35339  lnjatN  35504  lncvrat  35506  cdlemblem  35517  elpaddri  35526  paddasslem2  35545  paddasslem16  35559  padd4N  35564  hlmod1i  35580  dalawlem2  35596  pclfinN  35624  pexmidlem4N  35697  pl42lem1N  35703  lhp2lt  35725  lhpexle1  35732  lhpexle2lem  35733  lhpj1  35746  lhpmcvr5N  35751  lhp2at0  35756  lhp2atnle  35757  lhp2at0nle  35759  lhple  35766  lhpat  35767  lhpat4N  35768  4atexlempnq  35779  4atexlem7  35799  4atex  35800  ltrn11  35850  ltrnle  35853  ltrnm  35855  ltrnj  35856  ltrncvr  35857  ltrnel  35863  ltrncnvel  35866  ltrncnv  35870  ltrnmwOLD  35876  trlval2  35888  trlcnv  35890  trljat1  35891  trljat2  35892  trlat  35894  trl0  35895  trlnidat  35898  trlnid  35904  cdlemc1  35916  cdlemc2  35917  cdlemc5  35920  cdlemd2  35924  cdlemd7  35929  cdlemd8  35930  cdlemd9  35931  cdleme0e  35942  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme5  35965  cdleme10  35979  cdleme11a  35985  cdleme11c  35986  cdleme11h  35991  cdleme11j  35992  cdleme0nex  36015  cdleme18a  36016  cdleme18b  36017  cdleme22gb  36019  cdleme20zN  36026  cdleme20yOLD  36028  cdleme20c  36037  cdleme20k  36045  cdleme21a  36051  cdleme21b  36052  cdleme21c  36053  cdleme21h  36060  cdleme22b  36067  cdleme22d  36069  cdleme22f  36072  cdleme25a  36079  cdleme25c  36081  cdleme25dN  36082  cdleme26ee  36086  cdleme30a  36104  cdlemefr29bpre0N  36132  cdlemefr29clN  36133  cdlemefr32fvaN  36135  cdlemefr32fva1  36136  cdlemefs29bpre0N  36142  cdlemefs29bpre1N  36143  cdlemefs29cpre1N  36144  cdlemefs29clN  36145  cdleme43fsv1snlem  36146  cdlemefs32fvaN  36148  cdlemefs32fva1  36149  cdlemefs31fv1  36150  cdleme36a  36186  cdleme39a  36191  cdleme42a  36197  cdleme42c  36198  cdleme17d3  36222  cdleme48fv  36225  cdleme48bw  36228  cdleme48b  36229  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemeg46gfv  36256  cdleme48d  36261  cdleme50trn2a  36276  cdleme50trn2  36277  cdleme50ltrn  36283  cdlemf1  36287  cdlemf  36289  trlord  36295  cdlemg2dN  36316  cdlemg2fvlem  36320  cdlemg2l  36329  cdlemg7fvbwN  36333  cdlemg7aN  36351  cdlemg10bALTN  36362  cdlemg10c  36365  cdlemg17a  36387  cdlemg17dALTN  36390  cdlemg31b0a  36421  cdlemg31a  36423  cdlemg31b  36424  cdlemg34  36438  cdlemg36  36440  ltrnco  36445  trlcoabs2N  36448  trlcolem  36452  cdlemg48  36463  tgrpov  36474  tendoco2  36494  tendoplco2  36505  cdlemh1  36541  cdlemi1  36544  cdlemi2  36545  cdlemj3  36549  tendoid0  36551  cdlemk1  36557  cdlemk2  36558  cdlemk4  36560  cdlemk8  36564  cdlemk9  36565  cdlemk9bN  36566  cdlemk10  36569  cdlemk26b-3  36631  cdlemk26-3  36632  cdlemk28-3  36634  cdlemk37  36640  cdlemk39  36642  cdlemkfid1N  36647  cdlemkid1  36648  cdlemky  36652  cdlemkyu  36653  cdlemk19ylem  36656  cdlemk19xlem  36668  cdlemk11t  36672  cdlemk51  36679  cdlemkyyN  36688  cdleml6  36707  cdleml7  36708  cdleml8  36709  cdleml9  36710  erngdvlem4  36717  erngdvlem4-rN  36725  tendospcanN  36750  dia11N  36775  cdlemm10N  36845  dib11N  36887  dicvaddcl  36917  dicvscacl  36918  cdlemn6  36929  dihvalcq2  36974  dihopelvalcpre  36975  dihord6b  36987  dihord5apre  36989  dihmeetlem1N  37017  dihmeetlem2N  37026  dihglbcpreN  37027  dihjatc1  37038  dihmeetlem20N  37053  dih1dimatlem0  37055  dihatlat  37061  dihglblem6  37067  dochexmidlem4  37190  mapdpglem32  37432  mapdh8ad  37506  mapdh9aOLDN  37518  hdmap11lem2  37572  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