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

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

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 461 . 2
213ad2ant1 1017 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  simpl1r  1048  simpr1r  1054  simp11r  1108  simp21r  1114  simp31r  1120  vtoclgft  3157  funprg  5642  omeulem2  7251  uniinqs  7410  unxpdomlem3  7746  elfiun  7910  cofsmo  8670  isfin2-2  8720  isf32lem9  8762  tskun  9185  tskurn  9188  reclem3pr  9448  dedekind  9765  dmdcan  10279  lt2msq1  10453  supmullem1  10534  supmul  10536  xaddass2  11471  xlt2add  11481  xmulasslem3  11507  iccsplit  11682  expaddzlem  12209  expaddz  12210  expmulz  12212  limsupgle  13300  o1add  13436  o1mul  13437  o1sub  13438  bitsfzo  14085  sadfval  14102  smufval  14127  prmexpb  14258  4sqlem18  14480  vdwlem10  14508  mrieqv2d  15036  curf1  15494  mndodcong  16566  subgabl  16844  gex2abl  16857  cntzsubr  17461  abvres  17488  lbsind2  17727  lbsextlem2  17805  lbsextg  17808  matring  18945  mdetunilem8  19121  maducoeval  19141  maducoeval2  19142  madurid  19146  cramerimplem3  19187  pmatcollpw2  19279  pm2mpf1  19300  cnprest  19790  isreg2  19878  fbssfi  20338  hausflimlem  20480  tmdgsum  20594  ssblps  20925  ssbl  20926  xrsmopn  21317  dvres2  22316  vieta1  22708  aalioulem4  22731  efgh  22928  cxpadd  23060  cxpsub  23063  divcxp  23068  cxple2  23078  cxplt2  23079  cxpcn3lem  23121  angcan  23134  ang180lem5  23145  isosctrlem3  23154  brbtwn2  24208  axcontlem4  24270  axcontlem8  24274  clwwlknimp  24776  chscllem4  26558  ogrpinvlt  27714  pstmval  27874  measinblem  28191  cvmlift2lem6  28753  poseq  29333  linethru  29803  cnres2  30259  pellfundex  30822  congtr  30903  fzmaxdif  30919  isnumbasgrplem2  31053  idomsubgmo  31155  upbdrech  31505  mullimc  31622  islptre  31625  mullimcf  31629  neglimc  31653  icccncfext  31690  dvmptfprod  31742  stoweidlem31  31813  domnmsuppn0  32962  mndpfsupp  32969  lincext3  33057  lcv1  34766  lfl1  34795  lshpkrex  34843  hlrelat3  35136  cvrval3  35137  cvrval4N  35138  athgt  35180  atcvrlln2  35243  atcvrlln  35244  lvolnle3at  35306  lvolnlelpln  35309  4atlem11  35333  4atlem12  35336  2lplnj  35344  dalemddea  35408  cdlema2N  35516  paddasslem2  35545  atmod1i1m  35582  lhp2lt  35725  lhp0lt  35727  lhpexle3lem  35735  lhpj1  35746  lhpmcvr4N  35750  lhpelim  35761  lhpmod2i2  35762  lhpmod6i1  35763  cdlemb2  35765  lhpat  35767  ltrnatb  35861  ltrnel  35863  ltrncnvel  35866  ltrncnv  35870  ltrnmwOLD  35876  trlval2  35888  trljat1  35891  trljat2  35892  trlnidatb  35902  cdlemc1  35916  cdlemc2  35917  cdlemc5  35920  cdlemc6  35921  cdleme0aa  35935  cdleme0b  35937  cdleme0c  35938  cdleme0e  35942  cdleme0fN  35943  cdleme01N  35946  cdleme0ex1N  35948  cdleme0moN  35950  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme4  35963  cdleme4a  35964  cdleme5  35965  cdleme8  35975  cdleme9  35978  cdleme10  35979  cdleme16aN  35984  cdleme11fN  35989  cdleme11g  35990  cdleme11k  35993  cdleme13  35997  cdleme17c  36013  cdleme17d1  36014  cdleme18c  36018  cdleme22gb  36019  cdlemeda  36023  cdlemednpq  36024  cdlemednuN  36025  cdleme19c  36031  cdleme20aN  36035  cdleme20bN  36036  cdleme20c  36037  cdleme22aa  36065  cdleme22d  36069  cdleme22e  36070  cdleme27cl  36092  cdleme27a  36093  cdleme30a  36104  cdleme42a  36197  cdleme42c  36198  cdlemg2fv2  36326  cdlemg2m  36330  cdlemg4g  36342  cdlemg4  36343  cdlemg6c  36346  cdlemg7aN  36351  cdlemg9a  36358  cdlemg9b  36359  cdlemg10c  36365  cdlemg12a  36369  cdlemg12b  36370  cdlemg17a  36387  cdlemg18b  36405  cdlemg18c  36406  trlcoabs2N  36448  trlcolem  36452  tendoco2  36494  tendoicl  36522  cdlemi1  36544  cdlemi2  36545  cdlemj3  36549  tendocan  36550  cdlemk3  36559  cdlemk4  36560  cdlemk5a  36561  cdlemk9  36565  cdlemk9bN  36566  cdlemk10  36569  cdlemk30  36620  cdlemk31  36622  cdlemk39  36642  cdlemkfid1N  36647  cdlemkfid2N  36649  cdlemk19ylem  36656  cdlemk19xlem  36668  cdlemk53b  36682  cdlemk53  36683  cdlemk55a  36685  cdlemk43N  36689  cdlemk19u1  36695  cdlemm10N  36845  cdlemn2  36922  cdlemn10  36933  dihjustlem  36943  dihord2cN  36948  dihvalcq2  36974  dihopelvalcpre  36975  dihord5b  36986  dihord6b  36987  dihmeetlem2N  37026  dihmeetbclemN  37031  dihmeetlem4preN  37033  dihmeetALTN  37054  dochshpncl  37111  dochsatshpb  37179  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