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

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

Proof of Theorem simp2r
StepHypRef Expression
1 simpr 486 . 2 ((𝜓𝜒) → 𝜒)
213ad2ant2 1135 1 ((𝜑 ∧ (𝜓𝜒) ∧ 𝜃) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  simp12r  1288  simp22r  1294  simp32r  1300  fsnunf  7136  f1oiso2  7302  fnsuppres  8127  frrlem4  8225  omeulem2  8535  uniinqs  8743  unxpdomlem3  9203  sup0  9409  fin23lem11  10260  reclem3pr  10992  dedekind  11325  addid2  11345  subaddmulsub  11625  dmdcan  11872  xaddass2  13176  xlt2add  13186  xadddi2  13223  expaddzlem  14018  expaddz  14019  expmulz  14021  expdiv  14026  expmordi  14079  pfxeq  14591  ccatopth2  14612  relexpaddnn  14943  o1add  15503  o1mul  15504  o1sub  15505  ntrivcvgmul  15794  prmexpb  16603  pcpremul  16722  pcdiv  16731  pcqmul  16732  pcqdiv  16736  4sqlem12  16835  f1ocpbllem  17413  ercpbl  17438  erlecpbl  17439  latjlej12  18351  latmlem12  18367  latj4  18385  gsumsgrpccat  18657  symgsssg  19256  symgfisg  19257  mndodcong  19331  cmn4  19590  ablsub4  19598  abladdsub4  19599  lsm4  19645  abvdom  20313  abvtrivd  20315  lspsnvs  20591  lspsneu  20600  lspfixed  20605  lspexch  20606  lsmcv  20618  lspsolvlem  20619  mvrf1  21410  coe1sclmulfv  21670  m1detdiag  21962  cnprest  22656  isreg2  22744  elptr  22940  hausflimlem  23346  trcfilu  23662  ssblps  23791  ssbl  23792  prdsxmslem2  23901  tgqioo  24179  metnrm  24241  bndth  24337  ncvspi  24536  cph2ass  24593  iscau3  24658  ovolunlem2  24878  dvres2  25292  dvfsumlem2  25407  dvfsum2  25414  deg1tm  25499  plyadd  25594  plymul  25595  coeeu  25602  coemullem  25627  aalioulem4  25711  cxplea  26067  cxple2  26068  cxplt2  26069  cxple2a  26070  cxpcn3lem  26116  angcan  26168  ang180lem5  26179  divsqrtsumlem  26345  logexprlim  26589  dchrvmasumlema  26864  dchrisum0lema  26878  logdivsum  26897  log2sumbnd  26908  padicabv  26994  nolesgn2ores  27036  nogesgn1o  27037  nogesgn1ores  27038  nolt02o  27059  nogt01o  27060  nosupinfsep  27096  noetalem1  27105  noeta2  27146  scutbdaylt  27179  tghilberti2  27622  brbtwn2  27896  axcontlem4  27958  axcontlem8  27962  clwlkl1loop  28773  chscllem4  30624  mdslmd4i  31317  orngmul  32138  nexple  32648  measxun2  32849  measun  32850  mbfmco2  32905  probun  33059  satfv1fvfmla1  34057  wsuclem  34439  cgrcomim  34603  cgrcoml  34610  cgrcomr  34611  cgrdegen  34618  btwnintr  34633  btwnexch3  34634  btwnouttr  34638  btwnexch  34639  btwndiff  34641  ifscgr  34658  lineid  34697  btwnconn1lem7  34707  btwnconn1lem8  34708  btwnconn1lem9  34709  btwnconn1lem12  34712  midofsegid  34718  brsegle2  34723  btwnoutside  34739  outsideoftr  34743  cnres2  36251  heibor  36309  lsmsat  37499  lkrlsp  37593  lkrlsp2  37594  lkrlsp3  37595  lshpkrlem6  37606  latm4  37724  omlspjN  37752  hlatj4  37865  4noncolr3  37945  4noncolr2  37946  4noncolr1  37947  3dimlem3a  37952  3dimlem4a  37955  3dimlem4  37956  3dimlem4OLDN  37957  1cvratex  37965  hlatexch4  37973  3atlem4  37978  atcvrlln2  38011  atcvrlln  38012  llnmlplnN  38031  lplnnlelln  38035  lvoli2  38073  lvolnlelln  38076  lvolnlelpln  38077  4atlem11b  38100  4atlem12b  38103  2lplnj  38112  dalemzeo  38125  dath2  38229  lncvrat  38274  cdlemb  38286  elpaddri  38294  padd4N  38332  llnmod2i2  38355  llnexchb2  38361  dalawlem1  38363  dalawlem2  38364  osumcllem6N  38453  pexmidlem3N  38464  pexmidlem4N  38465  lhp2lt  38493  lhp2at0  38524  lhp2atne  38526  lhp2at0ne  38528  lhpmod2i2  38530  lhpmod6i1  38531  lhpat  38535  lhpat3  38538  4atexlemex6  38566  ltrncoval  38637  ltrncnv  38638  ltrnnidn  38666  cdlemd7  38696  cdleme0b  38704  cdleme0c  38705  cdleme0fN  38710  cdleme0ex1N  38715  cdleme7d  38738  cdleme7e  38739  cdleme7ga  38740  cdleme7  38741  cdleme11a  38752  cdleme17c  38780  cdleme22gb  38786  cdlemeda  38790  cdleme20k  38811  cdleme21a  38817  cdleme21at  38820  cdleme21d  38822  cdleme22f2  38839  cdleme22g  38840  cdleme24  38844  cdleme28  38865  cdlemefrs29cpre1  38890  cdlemefr29exN  38894  cdlemefr32sn2aw  38896  cdleme32fva  38929  cdleme32fva1  38930  cdleme35a  38940  cdleme42c  38964  cdleme42e  38971  cdleme42f  38972  cdleme42g  38973  cdleme42h  38974  cdleme43bN  38982  cdleme46f2g2  38985  cdleme17d2  38987  cdleme4gfv  38999  cdlemeg46c  39005  cdlemeg46nlpq  39009  cdlemeg46gfre  39024  cdlemeg49lebilem  39031  cdleme50trn1  39041  cdleme50trn2  39043  cdleme50ltrn  39049  cdleme  39052  cdlemf1  39053  cdlemf  39055  trlord  39061  ltrniotavalbN  39076  cdlemg1cex  39080  cdlemg2dN  39082  cdlemg2ce  39084  cdlemg2fvlem  39086  cdlemg2idN  39088  cdlemg2kq  39094  cdlemg2l  39095  cdlemg7fvN  39116  cdlemg7aN  39117  cdlemg8a  39119  cdlemg11aq  39130  cdlemg12d  39138  cdlemg13a  39143  cdlemg13  39144  cdlemg14f  39145  cdlemg14g  39146  cdlemg17b  39154  cdlemg27a  39184  cdlemg31b0N  39186  cdlemg31a  39189  cdlemg31b  39190  cdlemg31c  39191  ltrnco  39211  trlcoabs2N  39214  trlcocnvat  39216  trlconid  39217  trlcolem  39218  cdlemg42  39221  cdlemg43  39222  cdlemg47a  39226  cdlemg46  39227  cdlemg47  39228  tendoeq1  39256  tendocoval  39258  tendoco2  39260  tendoplco2  39271  tendopltp  39272  cdlemh1  39307  cdlemh2  39308  cdlemi1  39310  cdlemi  39312  cdlemk1  39323  cdlemk2  39324  cdlemk3  39325  cdlemk4  39326  cdlemk8  39330  cdlemk9  39331  cdlemk9bN  39332  cdlemk31  39388  cdlemk28-3  39400  cdlemk19xlem  39434  cdlemk39u  39460  cdlemk19u  39462  cdlemk56w  39465  cdlemn7  39695  cdlemn8  39696  cdlemn9  39697  dihordlem6  39705  dihordlem7  39706  dihordlem7b  39707  dihord1  39710  dihord2a  39711  dihord11c  39716  dihord2pre  39717  dihord2pre2  39718  dihlsscpre  39726  dihord4  39750  dihord6b  39752  dihmeetlem2N  39791  dihglbcpreN  39792  dihmeetcN  39794  dihmeetbclemN  39796  dihmeetlem3N  39797  dihmeetlem9N  39807  dihmeetlem13N  39811  dihmeetlem20N  39818  mapdpglem24  40196  mapdpglem32  40197  baerlem3lem2  40202  baerlem5alem2  40203  baerlem5blem2  40204  mapdh9aOLDN  40282  hdmap14lem6  40365  nnadddir  40815  sn-addid2  40902  mzpmfp  41099  mzpsubst  41100  pellexlem5  41185  pell14qrexpclnn0  41218  pellfundex  41238  qirropth  41260  monotuz  41294  congmul  41320  congsub  41323  mzpcong  41325  fzmaxdif  41334  jm2.15nn0  41356  idomsubgmo  41554  trclimalb2  42072  mnringmulrcld  42582  fourierdlem42  44464  fourierdlem48  44469  fourierdlem80  44501  prmdvdsfmtnof1lem1  45850  lidldomn1  46293  rngccatidALTV  46361  ringccatidALTV  46424  coe1sclmulval  46540  line2  46912  line2xlem  46913  line2x  46914  line2y  46915  itsclc0yqsol  46924  seposep  47032  iscnrm3rlem8  47054  iscnrm3llem2  47057
  Copyright terms: Public domain W3C validator