MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp2r Structured version   Visualization version   GIF version

Theorem simp2r 1219
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp2r ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 479 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 1126 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  simpl2rOLD  1262  simpr2rOLD  1274  simp12r  1348  simp22r  1354  simp32r  1360  funprgOLD  6090  fsnunf  6603  f1oiso2  6753  fnsuppres  7479  omeulem2  7820  uniinqs  7982  unxpdomlem3  8319  sup0  8525  fin23lem11  9302  reclem3pr  10034  dedekind  10363  addid2  10382  dmdcan  10898  xaddass2  12244  xlt2add  12254  xadddi2  12291  expaddzlem  13068  expaddz  13069  expmulz  13071  expdiv  13076  ccatopth2  13642  relexpaddnn  13961  o1add  14514  o1mul  14515  o1sub  14516  ntrivcvgmul  14804  prmexpb  15603  pcpremul  15721  pcdiv  15730  pcqmul  15731  pcqdiv  15735  4sqlem12  15833  f1ocpbllem  16357  ercpbl  16382  erlecpbl  16383  latjlej12  17239  latmlem12  17255  latj4  17273  symgsssg  18058  symgfisg  18059  mndodcong  18132  cmn4  18383  ablsub4  18389  abladdsub4  18390  lsm4  18434  abvdom  19011  abvtrivd  19013  lspsnvs  19287  lspsneu  19296  lspfixed  19301  lspexch  19302  lsmcv  19314  lspsolvlem  19315  mvrf1  19598  coe1sclmulfv  19826  m1detdiag  20576  cnprest  21266  isreg2  21354  elptr  21549  hausflimlem  21955  trcfilu  22270  ssblps  22399  ssbl  22400  prdsxmslem2  22506  tgqioo  22775  metnrm  22837  bndth  22929  ncvspi  23127  cph2ass  23184  iscau3  23247  ovolunlem2  23437  dvres2  23846  dvfsumlem2  23960  dvfsum2  23967  deg1tm  24048  plyadd  24143  plymul  24144  coeeu  24151  coemullem  24176  aalioulem4  24260  cxplea  24612  cxple2  24613  cxplt2  24614  cxple2a  24615  cxpcn3lem  24658  angcan  24702  ang180lem5  24713  divsqrtsumlem  24876  logexprlim  25120  dchrvmasumlema  25359  dchrisum0lema  25373  logdivsum  25392  log2sumbnd  25403  padicabv  25489  tghilberti2  25703  brbtwn2  25955  axcontlem4  26017  axcontlem8  26021  clwlkl1loop  26860  clwwlknonex2lem2  27228  chscllem4  28779  mdslmd4i  29472  orngmul  30083  nexple  30351  measxun2  30553  measun  30554  mbfmco2  30607  probun  30761  wsuclem  32047  frrlem4  32060  nolesgn2ores  32102  nolt02o  32122  noetalem5  32144  scutbdaylt  32199  cgrcomim  32373  cgrcoml  32380  cgrcomr  32381  cgrdegen  32388  btwnintr  32403  btwnexch3  32404  btwnouttr  32408  btwnexch  32409  btwndiff  32411  ifscgr  32428  lineid  32467  btwnconn1lem7  32477  btwnconn1lem8  32478  btwnconn1lem9  32479  btwnconn1lem12  32482  midofsegid  32488  brsegle2  32493  btwnoutside  32509  outsideoftr  32513  cnres2  33844  heibor  33902  lsmsat  34767  lkrlsp  34861  lkrlsp2  34862  lkrlsp3  34863  lshpkrlem6  34874  latm4  34992  omlspjN  35020  hlatj4  35132  4noncolr3  35211  4noncolr2  35212  4noncolr1  35213  3dimlem3a  35218  3dimlem4a  35221  3dimlem4  35222  3dimlem4OLDN  35223  1cvratex  35231  hlatexch4  35239  3atlem4  35244  atcvrlln2  35277  atcvrlln  35278  llnmlplnN  35297  lplnnlelln  35301  lvoli2  35339  lvolnlelln  35342  lvolnlelpln  35343  4atlem11b  35366  4atlem12b  35369  2lplnj  35378  dalemzeo  35391  dath2  35495  lncvrat  35540  cdlemb  35552  elpaddri  35560  padd4N  35598  llnmod2i2  35621  llnexchb2  35627  dalawlem1  35629  dalawlem2  35630  osumcllem6N  35719  pexmidlem3N  35730  pexmidlem4N  35731  lhp2lt  35759  lhp2at0  35790  lhp2atne  35792  lhp2at0ne  35794  lhpmod2i2  35796  lhpmod6i1  35797  lhpat  35801  lhpat3  35804  4atexlemex6  35832  ltrncoval  35903  ltrncnv  35904  ltrnnidn  35933  cdlemd7  35963  cdleme0b  35971  cdleme0c  35972  cdleme0fN  35977  cdleme0ex1N  35982  cdleme7d  36005  cdleme7e  36006  cdleme7ga  36007  cdleme7  36008  cdleme11a  36019  cdleme17c  36047  cdleme22gb  36053  cdlemeda  36057  cdleme20k  36078  cdleme21a  36084  cdleme21at  36087  cdleme21d  36089  cdleme22f2  36106  cdleme22g  36107  cdleme24  36111  cdleme28  36132  cdlemefrs29cpre1  36157  cdlemefr29exN  36161  cdlemefr32sn2aw  36163  cdleme32fva  36196  cdleme32fva1  36197  cdleme35a  36207  cdleme42c  36231  cdleme42e  36238  cdleme42f  36239  cdleme42g  36240  cdleme42h  36241  cdleme43bN  36249  cdleme46f2g2  36252  cdleme17d2  36254  cdleme4gfv  36266  cdlemeg46c  36272  cdlemeg46nlpq  36276  cdlemeg46gfre  36291  cdlemeg49lebilem  36298  cdleme50trn1  36308  cdleme50trn2  36310  cdleme50ltrn  36316  cdleme  36319  cdlemf1  36320  cdlemf  36322  trlord  36328  ltrniotavalbN  36343  cdlemg1cex  36347  cdlemg2dN  36349  cdlemg2ce  36351  cdlemg2fvlem  36353  cdlemg2idN  36355  cdlemg2kq  36361  cdlemg2l  36362  cdlemg7fvN  36383  cdlemg7aN  36384  cdlemg8a  36386  cdlemg11aq  36397  cdlemg12d  36405  cdlemg13a  36410  cdlemg13  36411  cdlemg14f  36412  cdlemg14g  36413  cdlemg17b  36421  cdlemg27a  36451  cdlemg31b0N  36453  cdlemg31a  36456  cdlemg31b  36457  cdlemg31c  36458  ltrnco  36478  trlcoabs2N  36481  trlcocnvat  36483  trlconid  36484  trlcolem  36485  cdlemg42  36488  cdlemg43  36489  cdlemg47a  36493  cdlemg46  36494  cdlemg47  36495  tendoeq1  36523  tendocoval  36525  tendoco2  36527  tendoplco2  36538  tendopltp  36539  cdlemh1  36574  cdlemh2  36575  cdlemi1  36577  cdlemi  36579  cdlemk1  36590  cdlemk2  36591  cdlemk3  36592  cdlemk4  36593  cdlemk8  36597  cdlemk9  36598  cdlemk9bN  36599  cdlemk31  36655  cdlemk28-3  36667  cdlemk19xlem  36701  cdlemk39u  36727  cdlemk19u  36729  cdlemk56w  36732  cdlemn7  36963  cdlemn8  36964  cdlemn9  36965  dihordlem6  36973  dihordlem7  36974  dihordlem7b  36975  dihord1  36978  dihord2a  36979  dihord11c  36984  dihord2pre  36985  dihord2pre2  36986  dihlsscpre  36994  dihord4  37018  dihord6b  37020  dihmeetlem2N  37059  dihglbcpreN  37060  dihmeetcN  37062  dihmeetbclemN  37064  dihmeetlem3N  37065  dihmeetlem9N  37075  dihmeetlem13N  37079  dihmeetlem20N  37086  mapdpglem24  37464  mapdpglem32  37465  baerlem3lem2  37470  baerlem5alem2  37471  baerlem5blem2  37472  mapdh9aOLDN  37551  hdmap14lem6  37636  mzpmfp  37781  mzpsubst  37782  pellexlem5  37868  pell14qrexpclnn0  37901  pellfundex  37921  qirropth  37944  monotuz  37977  expmordi  37983  congmul  38005  congsub  38008  mzpcong  38010  fzmaxdif  38019  jm2.15nn0  38041  idomsubgmo  38247  trclimalb2  38489  fourierdlem42  40838  fourierdlem48  40843  fourierdlem80  40875  prmdvdsfmtnof1lem1  41975  lidldomn1  42400  rngccatidALTV  42468  ringccatidALTV  42531  coe1sclmulval  42652
  Copyright terms: Public domain W3C validator