Theorem simp2r 1200

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 1087

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 1089

This theorem is referenced by:  simp12r  1287  simp22r  1293  simp32r  1299  fsnunf  7219  f1oiso2  7388  fnsuppres  8232  frrlem4  8330  omeulem2  8639  uniinqs  8855  unxpdomlem3  9315  sup0  9535  fin23lem11  10386  reclem3pr  11118  dedekind  11453  addlid  11473  subaddmulsub  11753  dmdcan  12004  xaddass2  13312  xlt2add  13322  xadddi2  13359  expaddzlem  14156  expaddz  14157  expmulz  14159  expdiv  14164  expmordi  14217  pfxeq  14744  ccatopth2  14765  relexpaddnn  15100  o1add  15660  o1mul  15661  o1sub  15662  ntrivcvgmul  15950  prmexpb  16766  pcpremul  16890  pcdiv  16899  pcqmul  16900  pcqdiv  16904  4sqlem12  17003  f1ocpbllem  17584  ercpbl  17609  erlecpbl  17610  latjlej12  18525  latmlem12  18541  latj4  18559  gsumsgrpccat  18875  symgsssg  19509  symgfisg  19510  mndodcong  19584  cmn4  19843  ablsub4  19852  abladdsub4  19853  lsm4  19902  abvdom  20853  abvtrivd  20855  lspsnvs  21139  lspsneu  21148  lspfixed  21153  lspexch  21154  lsmcv  21166  lspsolvlem  21167  mvrf1  22029  coe1sclmulfv  22307  m1detdiag  22624  cnprest  23318  isreg2  23406  elptr  23602  hausflimlem  24008  trcfilu  24324  ssblps  24453  ssbl  24454  prdsxmslem2  24563  tgqioo  24841  metnrm  24903  bndth  25009  ncvspi  25209  cph2ass  25266  iscau3  25331  ovolunlem2  25552  dvres2  25967  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsum2  26095  deg1tm  26178  plyadd  26276  plymul  26277  coeeu  26284  coemullem  26309  aalioulem4  26395  cxplea  26756  cxple2  26757  cxplt2  26758  cxple2a  26759  cxpcn3lem  26808  angcan  26863  ang180lem5  26874  divsqrtsumlem  27041  logexprlim  27287  dchrvmasumlema  27562  dchrisum0lema  27576  logdivsum  27595  log2sumbnd  27606  padicabv  27692  nolesgn2ores  27735  nogesgn1o  27736  nogesgn1ores  27737  nolt02o  27758  nogt01o  27759  nosupinfsep  27795  noetalem1  27804  noeta2  27847  scutbdaylt  27881  expsgt0  28433  tghilberti2  28664  brbtwn2  28938  axcontlem4  29000  axcontlem8  29004  clwlkl1loop  29819  chscllem4  31672  mdslmd4i  32365  orngmul  33298  nexple  33973  measxun2  34174  measun  34175  mbfmco2  34230  probun  34384  satfv1fvfmla1  35391  wsuclem  35789  cgrcomim  35953  cgrcoml  35960  cgrcomr  35961  cgrdegen  35968  btwnintr  35983  btwnexch3  35984  btwnouttr  35988  btwnexch  35989  btwndiff  35991  ifscgr  36008  lineid  36047  btwnconn1lem7  36057  btwnconn1lem8  36058  btwnconn1lem9  36059  btwnconn1lem12  36062  midofsegid  36068  brsegle2  36073  btwnoutside  36089  outsideoftr  36093  cnres2  37723  heibor  37781  lsmsat  38964  lkrlsp  39058  lkrlsp2  39059  lkrlsp3  39060  lshpkrlem6  39071  latm4  39189  omlspjN  39217  hlatj4  39330  4noncolr3  39410  4noncolr2  39411  4noncolr1  39412  3dimlem3a  39417  3dimlem4a  39420  3dimlem4  39421  3dimlem4OLDN  39422  1cvratex  39430  hlatexch4  39438  3atlem4  39443  atcvrlln2  39476  atcvrlln  39477  llnmlplnN  39496  lplnnlelln  39500  lvoli2  39538  lvolnlelln  39541  lvolnlelpln  39542  4atlem11b  39565  4atlem12b  39568  2lplnj  39577  dalemzeo  39590  dath2  39694  lncvrat  39739  cdlemb  39751  elpaddri  39759  padd4N  39797  llnmod2i2  39820  llnexchb2  39826  dalawlem1  39828  dalawlem2  39829  osumcllem6N  39918  pexmidlem3N  39929  pexmidlem4N  39930  lhp2lt  39958  lhp2at0  39989  lhp2atne  39991  lhp2at0ne  39993  lhpmod2i2  39995  lhpmod6i1  39996  lhpat  40000  lhpat3  40003  4atexlemex6  40031  ltrncoval  40102  ltrncnv  40103  ltrnnidn  40131  cdlemd7  40161  cdleme0b  40169  cdleme0c  40170  cdleme0fN  40175  cdleme0ex1N  40180  cdleme7d  40203  cdleme7e  40204  cdleme7ga  40205  cdleme7  40206  cdleme11a  40217  cdleme17c  40245  cdleme22gb  40251  cdlemeda  40255  cdleme20k  40276  cdleme21a  40282  cdleme21at  40285  cdleme21d  40287  cdleme22f2  40304  cdleme22g  40305  cdleme24  40309  cdleme28  40330  cdlemefrs29cpre1  40355  cdlemefr29exN  40359  cdlemefr32sn2aw  40361  cdleme32fva  40394  cdleme32fva1  40395  cdleme35a  40405  cdleme42c  40429  cdleme42e  40436  cdleme42f  40437  cdleme42g  40438  cdleme42h  40439  cdleme43bN  40447  cdleme46f2g2  40450  cdleme17d2  40452  cdleme4gfv  40464  cdlemeg46c  40470  cdlemeg46nlpq  40474  cdlemeg46gfre  40489  cdlemeg49lebilem  40496  cdleme50trn1  40506  cdleme50trn2  40508  cdleme50ltrn  40514  cdleme  40517  cdlemf1  40518  cdlemf  40520  trlord  40526  ltrniotavalbN  40541  cdlemg1cex  40545  cdlemg2dN  40547  cdlemg2ce  40549  cdlemg2fvlem  40551  cdlemg2idN  40553  cdlemg2kq  40559  cdlemg2l  40560  cdlemg7fvN  40581  cdlemg7aN  40582  cdlemg8a  40584  cdlemg11aq  40595  cdlemg12d  40603  cdlemg13a  40608  cdlemg13  40609  cdlemg14f  40610  cdlemg14g  40611  cdlemg17b  40619  cdlemg27a  40649  cdlemg31b0N  40651  cdlemg31a  40654  cdlemg31b  40655  cdlemg31c  40656  ltrnco  40676  trlcoabs2N  40679  trlcocnvat  40681  trlconid  40682  trlcolem  40683  cdlemg42  40686  cdlemg43  40687  cdlemg47a  40691  cdlemg46  40692  cdlemg47  40693  tendoeq1  40721  tendocoval  40723  tendoco2  40725  tendoplco2  40736  tendopltp  40737  cdlemh1  40772  cdlemh2  40773  cdlemi1  40775  cdlemi  40777  cdlemk1  40788  cdlemk2  40789  cdlemk3  40790  cdlemk4  40791  cdlemk8  40795  cdlemk9  40796  cdlemk9bN  40797  cdlemk31  40853  cdlemk28-3  40865  cdlemk19xlem  40899  cdlemk39u  40925  cdlemk19u  40927  cdlemk56w  40930  cdlemn7  41160  cdlemn8  41161  cdlemn9  41162  dihordlem6  41170  dihordlem7  41171  dihordlem7b  41172  dihord1  41175  dihord2a  41176  dihord11c  41181  dihord2pre  41182  dihord2pre2  41183  dihlsscpre  41191  dihord4  41215  dihord6b  41217  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetcN  41259  dihmeetbclemN  41261  dihmeetlem3N  41262  dihmeetlem9N  41272  dihmeetlem13N  41276  dihmeetlem20N  41283  mapdpglem24  41661  mapdpglem32  41662  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  mapdh9aOLDN  41747  hdmap14lem6  41830  nnadddir  42259  sn-addlid  42380  mzpmfp  42703  mzpsubst  42704  pellexlem5  42789  pell14qrexpclnn0  42822  pellfundex  42842  qirropth  42864  monotuz  42898  congmul  42924  congsub  42927  mzpcong  42929  fzmaxdif  42938  jm2.15nn0  42960  idomsubgmo  43154  trclimalb2  43688  mnringmulrcld  44197  fourierdlem42  46070  fourierdlem48  46075  fourierdlem80  46107  prmdvdsfmtnof1lem1  47458  lidldomn1  47954  rngccatidALTV  47995  ringccatidALTV  48029  coe1sclmulval  48114  line2  48486  line2xlem  48487  line2x  48488  line2y  48489  itsclc0yqsol  48498  seposep  48605  iscnrm3rlem8  48627  iscnrm3llem2  48630