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

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

Proof of Theorem simp3r
StepHypRef Expression
1 simpr 461 . 2
213ad2ant3 1019 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpl3r  1052  simpr3r  1058  simp13r  1112  simp23r  1118  simp33r  1124  disjss3  4451  f1oiso2  6248  tfisi  6693  tfrlem5  7068  omeulem1  7250  omeulem2  7251  elfiun  7910  isfin2-2  8720  addid2  9784  mulcan  10211  mulcan2  10212  divass  10250  divdir  10255  div11  10258  ltdiv1  10431  ltmuldiv  10440  lediv2  10460  xaddass2  11471  xlt2add  11481  expaddz  12210  expmulz  12212  resqrex  13084  resqrtcl  13087  o1add  13436  o1mul  13437  o1sub  13438  dvdsgcd  14181  rpexp12i  14263  pythagtriplem4  14343  pythagtriplem11  14349  pythagtriplem13  14351  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  odcong  16573  cmn4  16817  ablsub4  16823  abladdsub4  16824  lsm4  16866  abvdom  17487  abvtrivd  17489  lspsolvlem  17788  lbsextlem2  17805  lidlsubcl  17863  frlmbas3  18807  matinvgcell  18937  matmulcell  18947  ma1repveval  19073  mdetunilem3  19116  mdetuni0  19123  mdetmul  19125  hausflimlem  20480  psmetlecl  20819  xmetlecl  20849  prdsxmetlem  20871  xblcntrps  20913  xblcntr  20914  bndth  21458  cph2ass  21659  iscau3  21717  dvres2  22316  coemullem  22647  vieta1  22708  aalioulem4  22731  cxpcn3lem  23121  angcan  23134  divsqrtsumlem  23309  dchrmusumlema  23678  dchrvmasumlema  23685  dchrisum0lema  23699  logdivsum  23718  padicabv  23815  ax5seglem3  24234  ax5seglem6  24237  axpasch  24244  axeuclid  24266  axcontlem4  24270  axcontlem8  24274  gxnval  25262  gxnn0mul  25279  adjlnop  27005  xreceu  27618  orngmul  27793  rhmdvd  27811  measvunilem  28183  measvuni  28185  cgrcomim  29639  cgrcoml  29646  cgrcomr  29647  cgrdegen  29654  segconeu  29661  btwnintr  29669  btwnexch3  29670  btwnouttr2  29672  btwnouttr  29674  btwnexch  29675  ifscgr  29694  lineext  29726  linecgr  29731  lineid  29733  idinside  29734  btwnconn1lem3  29739  btwnconn1lem4  29740  btwnconn1lem14  29750  btwnconn2  29752  btwnconn3  29753  midofsegid  29754  btwnoutside  29775  outsideoftr  29779  lineunray  29797  lineelsb2  29798  itg2addnclem  30066  cnres2  30259  heibor  30317  mzpmfp  30679  mzpmfpOLD  30680  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  mullimcf  31629  addlimc  31654  0ellimcdiv  31655  fourierdlem48  31937  fourierdlem80  31969  lincfsuppcl  33014  lindslinindimp2lem3  33061  bnj1128  34046  lsmcv2  34754  lcvat  34755  lcvexchlem4  34762  lcvexchlem5  34763  lfladd  34791  lflsub  34792  lflmul  34793  lshpkrlem4  34838  latm4  34958  omlmod1i2N  34985  cvlsupr7  35073  cvlsupr8  35074  hlatj4  35098  hlrelat3  35136  cvrval3  35137  atcvrj1  35155  atlelt  35162  2atlt  35163  2atjm  35169  3noncolr2  35173  athgt  35180  3dimlem2  35183  3dimlem4OLDN  35189  1cvratex  35197  ps-1  35201  ps-2  35202  hlatexch3N  35204  llnle  35242  atcvrlln2  35243  atcvrlln  35244  lplni2  35261  lplnle  35264  lplnnle2at  35265  lplnnlelln  35267  llncvrlpln2  35281  2llnmeqat  35295  lvolnle3at  35306  lvolnlelln  35308  4atlem0ae  35318  lneq2at  35502  lnjatN  35504  lncvrat  35506  2lnat  35508  elpaddri  35526  paddasslem2  35545  padd4N  35564  hlmod1i  35580  llnexchb2  35593  dalawlem2  35596  pclfinN  35624  pexmidlem4N  35697  pl42lem1N  35703  lhp2lt  35725  lhpexle1  35732  lhpexle2lem  35733  lhpj1  35746  lhpmcvr5N  35751  lhp2at0  35756  lhp2at0nle  35759  lhple  35766  lhpat  35767  lhpat4N  35768  4atexlemnslpq  35780  4atexlem7  35799  ltrn11  35850  ltrnle  35853  ltrnm  35855  ltrnj  35856  ltrncvr  35857  ltrnel  35863  ltrncnvel  35866  ltrncnv  35870  ltrnmwOLD  35876  trlat  35894  trl0  35895  trlnidat  35898  trlnid  35904  ltrnatlw  35908  trlne  35910  trlval4  35913  cdlemc5  35920  cdlemd2  35924  cdlemd7  35929  cdlemd8  35930  cdlemd9  35931  cdleme0c  35938  cdleme0e  35942  cdleme0fN  35943  cdleme3g  35959  cdleme3h  35960  cdleme5  35965  cdleme11c  35986  cdleme11h  35991  cdleme11j  35992  cdleme11k  35993  cdleme0nex  36015  cdleme18a  36016  cdleme22gb  36019  cdleme20zN  36026  cdleme20yOLD  36028  cdleme20c  36037  cdleme20k  36045  cdleme21a  36051  cdleme21b  36052  cdleme21c  36053  cdleme21ct  36055  cdleme21h  36060  cdleme22d  36069  cdleme22f  36072  cdleme26ee  36086  cdleme30a  36104  cdlemefs45eN  36157  cdleme36a  36186  cdleme36m  36187  cdleme39a  36191  cdleme42b  36204  cdleme43dN  36218  cdlemeg47rv2  36236  cdlemeg46sfg  36246  cdlemeg46rjgN  36248  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemeg46gfv  36256  cdleme48d  36261  cdleme50ltrn  36283  cdlemf1  36287  cdlemf  36289  cdlemg2dN  36316  cdlemg2fvlem  36320  cdlemg2l  36329  cdlemg7fvbwN  36333  cdlemg7aN  36351  cdlemg10c  36365  cdlemg17a  36387  cdlemg17dALTN  36390  cdlemg18a  36404  cdlemg18b  36405  cdlemg31b0a  36421  cdlemg31a  36423  cdlemg31b  36424  ltrnco  36445  cdlemg48  36463  tgrpov  36474  tendoco2  36494  tendoplco2  36505  cdlemh1  36541  cdlemk1  36557  cdlemk26b-3  36631  cdlemk27-3  36633  cdlemk28-3  36634  cdlemk34  36636  cdlemkfid1N  36647  cdlemkid3N  36659  cdlemkid4  36660  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk51  36679  tendospcanN  36750  cdlemm10N  36845  dicvaddcl  36917  dicvscacl  36918  cdlemn6  36929  dihvalcq2  36974  dihord6b  36987  dihord5apre  36989  dihglbcpreN  37027  dihjatc1  37038  dihmeetlem20N  37053  dih1dimatlem0  37055  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