Theorem simp2r 1201

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1134	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp12r  1288  simp22r  1294  simp32r  1300  fsnunf  7131  f1oiso2  7298  fnsuppres  8133  frrlem4  8231  omeulem2  8510  uniinqs  8734  unxpdomlem3  9158  sup0  9370  fin23lem11  10227  reclem3pr  10960  dedekind  11296  addlid  11316  subaddmulsub  11600  dmdcan  11851  xaddass2  13165  xlt2add  13175  xadddi2  13212  expaddzlem  14028  expaddz  14029  expmulz  14031  expdiv  14036  expmordi  14090  pfxeq  14619  ccatopth2  14640  relexpaddnn  14974  o1add  15537  o1mul  15538  o1sub  15539  ntrivcvgmul  15825  prmexpb  16646  pcpremul  16771  pcdiv  16780  pcqmul  16781  pcqdiv  16785  4sqlem12  16884  f1ocpbllem  17445  ercpbl  17470  erlecpbl  17471  latjlej12  18378  latmlem12  18394  latj4  18412  gsumsgrpccat  18765  symgsssg  19396  symgfisg  19397  mndodcong  19471  cmn4  19730  ablsub4  19739  abladdsub4  19740  lsm4  19789  abvdom  20763  abvtrivd  20765  orngmul  20798  lspsnvs  21069  lspsneu  21078  lspfixed  21083  lspexch  21084  lsmcv  21096  lspsolvlem  21097  mvrf1  21941  coe1sclmulfv  22225  m1detdiag  22541  cnprest  23233  isreg2  23321  elptr  23517  hausflimlem  23923  trcfilu  24237  ssblps  24366  ssbl  24367  prdsxmslem2  24473  tgqioo  24744  metnrm  24807  bndth  24913  ncvspi  25112  cph2ass  25169  iscau3  25234  ovolunlem2  25455  dvres2  25869  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsum2  25997  deg1tm  26080  plyadd  26178  plymul  26179  coeeu  26186  coemullem  26211  aalioulem4  26299  cxplea  26661  cxple2  26662  cxplt2  26663  cxple2a  26664  cxpcn3lem  26713  angcan  26768  ang180lem5  26779  divsqrtsumlem  26946  logexprlim  27192  dchrvmasumlema  27467  dchrisum0lema  27481  logdivsum  27500  log2sumbnd  27511  padicabv  27597  nolesgn2ores  27640  nogesgn1o  27641  nogesgn1ores  27642  nolt02o  27663  nogt01o  27664  nosupinfsep  27700  noetalem1  27709  noeta2  27757  cutbdaylt  27794  expsgt0  28433  bdayfinbndlem1  28463  tghilberti2  28710  brbtwn2  28978  axcontlem4  29040  axcontlem8  29044  clwlkl1loop  29856  chscllem4  31715  mdslmd4i  32408  nexple  32925  measxun2  34367  measun  34368  mbfmco2  34422  probun  34576  satfv1fvfmla1  35617  wsuclem  36017  cgrcomim  36183  cgrcoml  36190  cgrcomr  36191  cgrdegen  36198  btwnintr  36213  btwnexch3  36214  btwnouttr  36218  btwnexch  36219  btwndiff  36221  ifscgr  36238  lineid  36277  btwnconn1lem7  36287  btwnconn1lem8  36288  btwnconn1lem9  36289  btwnconn1lem12  36292  midofsegid  36298  brsegle2  36303  btwnoutside  36319  outsideoftr  36323  cnres2  37960  heibor  38018  lsmsat  39264  lkrlsp  39358  lkrlsp2  39359  lkrlsp3  39360  lshpkrlem6  39371  latm4  39489  omlspjN  39517  hlatj4  39630  4noncolr3  39709  4noncolr2  39710  4noncolr1  39711  3dimlem3a  39716  3dimlem4a  39719  3dimlem4  39720  3dimlem4OLDN  39721  1cvratex  39729  hlatexch4  39737  3atlem4  39742  atcvrlln2  39775  atcvrlln  39776  llnmlplnN  39795  lplnnlelln  39799  lvoli2  39837  lvolnlelln  39840  lvolnlelpln  39841  4atlem11b  39864  4atlem12b  39867  2lplnj  39876  dalemzeo  39889  dath2  39993  lncvrat  40038  cdlemb  40050  elpaddri  40058  padd4N  40096  llnmod2i2  40119  llnexchb2  40125  dalawlem1  40127  dalawlem2  40128  osumcllem6N  40217  pexmidlem3N  40228  pexmidlem4N  40229  lhp2lt  40257  lhp2at0  40288  lhp2atne  40290  lhp2at0ne  40292  lhpmod2i2  40294  lhpmod6i1  40295  lhpat  40299  lhpat3  40302  4atexlemex6  40330  ltrncoval  40401  ltrncnv  40402  ltrnnidn  40430  cdlemd7  40460  cdleme0b  40468  cdleme0c  40469  cdleme0fN  40474  cdleme0ex1N  40479  cdleme7d  40502  cdleme7e  40503  cdleme7ga  40504  cdleme7  40505  cdleme11a  40516  cdleme17c  40544  cdleme22gb  40550  cdlemeda  40554  cdleme20k  40575  cdleme21a  40581  cdleme21at  40584  cdleme21d  40586  cdleme22f2  40603  cdleme22g  40604  cdleme24  40608  cdleme28  40629  cdlemefrs29cpre1  40654  cdlemefr29exN  40658  cdlemefr32sn2aw  40660  cdleme32fva  40693  cdleme32fva1  40694  cdleme35a  40704  cdleme42c  40728  cdleme42e  40735  cdleme42f  40736  cdleme42g  40737  cdleme42h  40738  cdleme43bN  40746  cdleme46f2g2  40749  cdleme17d2  40751  cdleme4gfv  40763  cdlemeg46c  40769  cdlemeg46nlpq  40773  cdlemeg46gfre  40788  cdlemeg49lebilem  40795  cdleme50trn1  40805  cdleme50trn2  40807  cdleme50ltrn  40813  cdleme  40816  cdlemf1  40817  cdlemf  40819  trlord  40825  ltrniotavalbN  40840  cdlemg1cex  40844  cdlemg2dN  40846  cdlemg2ce  40848  cdlemg2fvlem  40850  cdlemg2idN  40852  cdlemg2kq  40858  cdlemg2l  40859  cdlemg7fvN  40880  cdlemg7aN  40881  cdlemg8a  40883  cdlemg11aq  40894  cdlemg12d  40902  cdlemg13a  40907  cdlemg13  40908  cdlemg14f  40909  cdlemg14g  40910  cdlemg17b  40918  cdlemg27a  40948  cdlemg31b0N  40950  cdlemg31a  40953  cdlemg31b  40954  cdlemg31c  40955  ltrnco  40975  trlcoabs2N  40978  trlcocnvat  40980  trlconid  40981  trlcolem  40982  cdlemg42  40985  cdlemg43  40986  cdlemg47a  40990  cdlemg46  40991  cdlemg47  40992  tendoeq1  41020  tendocoval  41022  tendoco2  41024  tendoplco2  41035  tendopltp  41036  cdlemh1  41071  cdlemh2  41072  cdlemi1  41074  cdlemi  41076  cdlemk1  41087  cdlemk2  41088  cdlemk3  41089  cdlemk4  41090  cdlemk8  41094  cdlemk9  41095  cdlemk9bN  41096  cdlemk31  41152  cdlemk28-3  41164  cdlemk19xlem  41198  cdlemk39u  41224  cdlemk19u  41226  cdlemk56w  41229  cdlemn7  41459  cdlemn8  41460  cdlemn9  41461  dihordlem6  41469  dihordlem7  41470  dihordlem7b  41471  dihord1  41474  dihord2a  41475  dihord11c  41480  dihord2pre  41481  dihord2pre2  41482  dihlsscpre  41490  dihord4  41514  dihord6b  41516  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetcN  41558  dihmeetbclemN  41560  dihmeetlem3N  41561  dihmeetlem9N  41571  dihmeetlem13N  41575  dihmeetlem20N  41582  mapdpglem24  41960  mapdpglem32  41961  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  mapdh9aOLDN  42046  hdmap14lem6  42129  nnadddir  42521  sn-addlid  42655  mzpmfp  42985  mzpsubst  42986  pellexlem5  43071  pell14qrexpclnn0  43104  pellfundex  43124  qirropth  43146  monotuz  43179  congmul  43205  congsub  43208  mzpcong  43210  fzmaxdif  43219  jm2.15nn0  43241  idomsubgmo  43431  trclimalb2  43963  mnringmulrcld  44465  fourierdlem42  46389  fourierdlem48  46394  fourierdlem80  46426  prmdvdsfmtnof1lem1  47826  cycldlenngric  48170  gpgedgvtx1  48304  lidldomn1  48473  rngccatidALTV  48514  ringccatidALTV  48548  coe1sclmulval  48627  line2  48994  line2xlem  48995  line2x  48996  line2y  48997  itsclc0yqsol  49006  seposep  49167  iscnrm3rlem8  49188  iscnrm3llem2  49191