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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 476 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 1103 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  simpl2r  1135  simpr2r  1141  simp12r  1195  simp22r  1201  simp32r  1207  funprgOLD  5979  fsnunf  6492  f1oiso2  6642  fnsuppres  7367  omeulem2  7708  uniinqs  7870  unxpdomlem3  8207  sup0  8413  fin23lem11  9177  reclem3pr  9909  dedekind  10238  addid2  10257  dmdcan  10773  xaddass2  12118  xlt2add  12128  xadddi2  12165  expaddzlem  12943  expaddz  12944  expmulz  12946  expdiv  12951  ccatopth2  13517  relexpaddnn  13835  o1add  14388  o1mul  14389  o1sub  14390  ntrivcvgmul  14678  prmexpb  15477  pcpremul  15595  pcdiv  15604  pcqmul  15605  pcqdiv  15609  4sqlem12  15707  f1ocpbllem  16231  ercpbl  16256  erlecpbl  16257  latjlej12  17114  latmlem12  17130  latj4  17148  symgsssg  17933  symgfisg  17934  mndodcong  18007  cmn4  18258  ablsub4  18264  abladdsub4  18265  lsm4  18309  abvdom  18886  abvtrivd  18888  lspsnvs  19162  lspsneu  19171  lspfixed  19176  lspexch  19177  lsmcv  19189  lspsolvlem  19190  mvrf1  19473  coe1sclmulfv  19701  m1detdiag  20451  cnprest  21141  isreg2  21229  elptr  21424  hausflimlem  21830  trcfilu  22145  ssblps  22274  ssbl  22275  prdsxmslem2  22381  tgqioo  22650  metnrm  22712  bndth  22804  ncvspi  23002  cph2ass  23059  iscau3  23122  ovolunlem2  23312  dvres2  23721  dvfsumlem2  23835  dvfsum2  23842  deg1tm  23923  plyadd  24018  plymul  24019  coeeu  24026  coemullem  24051  aalioulem4  24135  cxplea  24487  cxple2  24488  cxplt2  24489  cxple2a  24490  cxpcn3lem  24533  angcan  24577  ang180lem5  24588  divsqrtsumlem  24751  logexprlim  24995  dchrvmasumlema  25234  dchrisum0lema  25248  logdivsum  25267  log2sumbnd  25278  padicabv  25364  tghilberti2  25578  brbtwn2  25830  axcontlem4  25892  axcontlem8  25896  clwlkl1loop  26734  clwwlknonex2lem2  27083  chscllem4  28627  mdslmd4i  29320  orngmul  29931  nexple  30199  measxun2  30401  measun  30402  mbfmco2  30455  probun  30609  wsuclem  31895  frrlem4  31908  nolesgn2ores  31950  nolt02o  31970  noetalem5  31992  scutbdaylt  32047  cgrcomim  32221  cgrcoml  32228  cgrcomr  32229  cgrdegen  32236  btwnintr  32251  btwnexch3  32252  btwnouttr  32256  btwnexch  32257  btwndiff  32259  ifscgr  32276  lineid  32315  btwnconn1lem7  32325  btwnconn1lem8  32326  btwnconn1lem9  32327  btwnconn1lem12  32330  midofsegid  32336  brsegle2  32341  btwnoutside  32357  outsideoftr  32361  cnres2  33692  heibor  33750  lsmsat  34613  lkrlsp  34707  lkrlsp2  34708  lkrlsp3  34709  lshpkrlem6  34720  latm4  34838  omlspjN  34866  hlatj4  34978  4noncolr3  35057  4noncolr2  35058  4noncolr1  35059  3dimlem3a  35064  3dimlem4a  35067  3dimlem4  35068  3dimlem4OLDN  35069  1cvratex  35077  hlatexch4  35085  3atlem4  35090  atcvrlln2  35123  atcvrlln  35124  llnmlplnN  35143  lplnnlelln  35147  lvoli2  35185  lvolnlelln  35188  lvolnlelpln  35189  4atlem11b  35212  4atlem12b  35215  2lplnj  35224  dalemzeo  35237  dath2  35341  lncvrat  35386  cdlemb  35398  elpaddri  35406  padd4N  35444  llnmod2i2  35467  llnexchb2  35473  dalawlem1  35475  dalawlem2  35476  osumcllem6N  35565  pexmidlem3N  35576  pexmidlem4N  35577  lhp2lt  35605  lhp2at0  35636  lhp2atne  35638  lhp2at0ne  35640  lhpmod2i2  35642  lhpmod6i1  35643  lhpat  35647  lhpat3  35650  4atexlemex6  35678  ltrncoval  35749  ltrncnv  35750  ltrnnidn  35779  cdlemd7  35809  cdleme0b  35817  cdleme0c  35818  cdleme0fN  35823  cdleme0ex1N  35828  cdleme7d  35851  cdleme7e  35852  cdleme7ga  35853  cdleme7  35854  cdleme11a  35865  cdleme17c  35893  cdleme22gb  35899  cdlemeda  35903  cdleme20k  35924  cdleme21a  35930  cdleme21at  35933  cdleme21d  35935  cdleme22f2  35952  cdleme22g  35953  cdleme24  35957  cdleme28  35978  cdlemefrs29cpre1  36003  cdlemefr29exN  36007  cdlemefr32sn2aw  36009  cdleme32fva  36042  cdleme32fva1  36043  cdleme35a  36053  cdleme42c  36077  cdleme42e  36084  cdleme42f  36085  cdleme42g  36086  cdleme42h  36087  cdleme43bN  36095  cdleme46f2g2  36098  cdleme17d2  36100  cdleme4gfv  36112  cdlemeg46c  36118  cdlemeg46nlpq  36122  cdlemeg46gfre  36137  cdlemeg49lebilem  36144  cdleme50trn1  36154  cdleme50trn2  36156  cdleme50ltrn  36162  cdleme  36165  cdlemf1  36166  cdlemf  36168  trlord  36174  ltrniotavalbN  36189  cdlemg1cex  36193  cdlemg2dN  36195  cdlemg2ce  36197  cdlemg2fvlem  36199  cdlemg2idN  36201  cdlemg2kq  36207  cdlemg2l  36208  cdlemg7fvN  36229  cdlemg7aN  36230  cdlemg8a  36232  cdlemg11aq  36243  cdlemg12d  36251  cdlemg13a  36256  cdlemg13  36257  cdlemg14f  36258  cdlemg14g  36259  cdlemg17b  36267  cdlemg27a  36297  cdlemg31b0N  36299  cdlemg31a  36302  cdlemg31b  36303  cdlemg31c  36304  ltrnco  36324  trlcoabs2N  36327  trlcocnvat  36329  trlconid  36330  trlcolem  36331  cdlemg42  36334  cdlemg43  36335  cdlemg47a  36339  cdlemg46  36340  cdlemg47  36341  tendoeq1  36369  tendocoval  36371  tendoco2  36373  tendoplco2  36384  tendopltp  36385  cdlemh1  36420  cdlemh2  36421  cdlemi1  36423  cdlemi  36425  cdlemk1  36436  cdlemk2  36437  cdlemk3  36438  cdlemk4  36439  cdlemk8  36443  cdlemk9  36444  cdlemk9bN  36445  cdlemk31  36501  cdlemk28-3  36513  cdlemk19xlem  36547  cdlemk39u  36573  cdlemk19u  36575  cdlemk56w  36578  cdlemn7  36809  cdlemn8  36810  cdlemn9  36811  dihordlem6  36819  dihordlem7  36820  dihordlem7b  36821  dihord1  36824  dihord2a  36825  dihord11c  36830  dihord2pre  36831  dihord2pre2  36832  dihlsscpre  36840  dihord4  36864  dihord6b  36866  dihmeetlem2N  36905  dihglbcpreN  36906  dihmeetcN  36908  dihmeetbclemN  36910  dihmeetlem3N  36911  dihmeetlem9N  36921  dihmeetlem13N  36925  dihmeetlem20N  36932  mapdpglem24  37310  mapdpglem32  37311  baerlem3lem2  37316  baerlem5alem2  37317  baerlem5blem2  37318  mapdh9aOLDN  37397  hdmap14lem6  37482  mzpmfp  37627  mzpsubst  37628  pellexlem5  37714  pell14qrexpclnn0  37747  pellfundex  37767  qirropth  37790  monotuz  37823  expmordi  37829  congmul  37851  congsub  37854  mzpcong  37856  fzmaxdif  37865  jm2.15nn0  37887  idomsubgmo  38093  trclimalb2  38335  fourierdlem42  40684  fourierdlem48  40689  fourierdlem80  40721  prmdvdsfmtnof1lem1  41821  lidldomn1  42246  rngccatidALTV  42314  ringccatidALTV  42377  coe1sclmulval  42498
  Copyright terms: Public domain W3C validator