Theorem simp2r 1202

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 1135	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  1289  simp22r  1295  simp32r  1301  fsnunf  7140  f1oiso2  7307  fnsuppres  8141  frrlem4  8239  omeulem2  8518  uniinqs  8744  unxpdomlem3  9168  sup0  9380  fin23lem11  10239  reclem3pr  10972  dedekind  11309  addlid  11329  subaddmulsub  11613  dmdcan  11865  nnadddir  12233  xaddass2  13202  xlt2add  13212  xadddi2  13249  expaddzlem  14067  expaddz  14068  expmulz  14070  expdiv  14075  expmordi  14129  pfxeq  14658  ccatopth2  14679  relexpaddnn  15013  o1add  15576  o1mul  15577  o1sub  15578  ntrivcvgmul  15867  prmexpb  16689  pcpremul  16814  pcdiv  16823  pcqmul  16824  pcqdiv  16828  4sqlem12  16927  f1ocpbllem  17488  ercpbl  17513  erlecpbl  17514  latjlej12  18421  latmlem12  18437  latj4  18455  gsumsgrpccat  18808  symgsssg  19442  symgfisg  19443  mndodcong  19517  cmn4  19776  ablsub4  19785  abladdsub4  19786  lsm4  19835  abvdom  20807  abvtrivd  20809  orngmul  20842  lspsnvs  21112  lspsneu  21121  lspfixed  21126  lspexch  21127  lsmcv  21139  lspsolvlem  21140  mvrf1  21964  coe1sclmulfv  22248  m1detdiag  22562  cnprest  23254  isreg2  23342  elptr  23538  hausflimlem  23944  trcfilu  24258  ssblps  24387  ssbl  24388  prdsxmslem2  24494  tgqioo  24765  metnrm  24828  bndth  24925  ncvspi  25123  cph2ass  25180  iscau3  25245  ovolunlem2  25465  dvres2  25879  dvfsumlem2  25994  dvfsum2  26001  deg1tm  26084  plyadd  26182  plymul  26183  coeeu  26190  coemullem  26215  aalioulem4  26301  cxplea  26660  cxple2  26661  cxplt2  26662  cxple2a  26663  cxpcn3lem  26711  angcan  26766  ang180lem5  26777  divsqrtsumlem  26943  logexprlim  27188  dchrvmasumlema  27463  dchrisum0lema  27477  logdivsum  27496  log2sumbnd  27507  padicabv  27593  nolesgn2ores  27636  nogesgn1o  27637  nogesgn1ores  27638  nolt02o  27659  nogt01o  27660  nosupinfsep  27696  noetalem1  27705  noeta2  27753  cutbdaylt  27790  expsgt0  28429  bdayfinbndlem1  28459  tghilberti2  28706  brbtwn2  28974  axcontlem4  29036  axcontlem8  29040  clwlkl1loop  29851  chscllem4  31711  mdslmd4i  32404  nexple  32917  measxun2  34354  measun  34355  mbfmco2  34409  probun  34563  satfv1fvfmla1  35605  wsuclem  36005  cgrcomim  36171  cgrcoml  36178  cgrcomr  36179  cgrdegen  36186  btwnintr  36201  btwnexch3  36202  btwnouttr  36206  btwnexch  36207  btwndiff  36209  ifscgr  36226  lineid  36265  btwnconn1lem7  36275  btwnconn1lem8  36276  btwnconn1lem9  36277  btwnconn1lem12  36280  midofsegid  36286  brsegle2  36291  btwnoutside  36307  outsideoftr  36311  ttcmin  36678  cnres2  38084  heibor  38142  lsmsat  39454  lkrlsp  39548  lkrlsp2  39549  lkrlsp3  39550  lshpkrlem6  39561  latm4  39679  omlspjN  39707  hlatj4  39820  4noncolr3  39899  4noncolr2  39900  4noncolr1  39901  3dimlem3a  39906  3dimlem4a  39909  3dimlem4  39910  3dimlem4OLDN  39911  1cvratex  39919  hlatexch4  39927  3atlem4  39932  atcvrlln2  39965  atcvrlln  39966  llnmlplnN  39985  lplnnlelln  39989  lvoli2  40027  lvolnlelln  40030  lvolnlelpln  40031  4atlem11b  40054  4atlem12b  40057  2lplnj  40066  dalemzeo  40079  dath2  40183  lncvrat  40228  cdlemb  40240  elpaddri  40248  padd4N  40286  llnmod2i2  40309  llnexchb2  40315  dalawlem1  40317  dalawlem2  40318  osumcllem6N  40407  pexmidlem3N  40418  pexmidlem4N  40419  lhp2lt  40447  lhp2at0  40478  lhp2atne  40480  lhp2at0ne  40482  lhpmod2i2  40484  lhpmod6i1  40485  lhpat  40489  lhpat3  40492  4atexlemex6  40520  ltrncoval  40591  ltrncnv  40592  ltrnnidn  40620  cdlemd7  40650  cdleme0b  40658  cdleme0c  40659  cdleme0fN  40664  cdleme0ex1N  40669  cdleme7d  40692  cdleme7e  40693  cdleme7ga  40694  cdleme7  40695  cdleme11a  40706  cdleme17c  40734  cdleme22gb  40740  cdlemeda  40744  cdleme20k  40765  cdleme21a  40771  cdleme21at  40774  cdleme21d  40776  cdleme22f2  40793  cdleme22g  40794  cdleme24  40798  cdleme28  40819  cdlemefrs29cpre1  40844  cdlemefr29exN  40848  cdlemefr32sn2aw  40850  cdleme32fva  40883  cdleme32fva1  40884  cdleme35a  40894  cdleme42c  40918  cdleme42e  40925  cdleme42f  40926  cdleme42g  40927  cdleme42h  40928  cdleme43bN  40936  cdleme46f2g2  40939  cdleme17d2  40941  cdleme4gfv  40953  cdlemeg46c  40959  cdlemeg46nlpq  40963  cdlemeg46gfre  40978  cdlemeg49lebilem  40985  cdleme50trn1  40995  cdleme50trn2  40997  cdleme50ltrn  41003  cdleme  41006  cdlemf1  41007  cdlemf  41009  trlord  41015  ltrniotavalbN  41030  cdlemg1cex  41034  cdlemg2dN  41036  cdlemg2ce  41038  cdlemg2fvlem  41040  cdlemg2idN  41042  cdlemg2kq  41048  cdlemg2l  41049  cdlemg7fvN  41070  cdlemg7aN  41071  cdlemg8a  41073  cdlemg11aq  41084  cdlemg12d  41092  cdlemg13a  41097  cdlemg13  41098  cdlemg14f  41099  cdlemg14g  41100  cdlemg17b  41108  cdlemg27a  41138  cdlemg31b0N  41140  cdlemg31a  41143  cdlemg31b  41144  cdlemg31c  41145  ltrnco  41165  trlcoabs2N  41168  trlcocnvat  41170  trlconid  41171  trlcolem  41172  cdlemg42  41175  cdlemg43  41176  cdlemg47a  41180  cdlemg46  41181  cdlemg47  41182  tendoeq1  41210  tendocoval  41212  tendoco2  41214  tendoplco2  41225  tendopltp  41226  cdlemh1  41261  cdlemh2  41262  cdlemi1  41264  cdlemi  41266  cdlemk1  41277  cdlemk2  41278  cdlemk3  41279  cdlemk4  41280  cdlemk8  41284  cdlemk9  41285  cdlemk9bN  41286  cdlemk31  41342  cdlemk28-3  41354  cdlemk19xlem  41388  cdlemk39u  41414  cdlemk19u  41416  cdlemk56w  41419  cdlemn7  41649  cdlemn8  41650  cdlemn9  41651  dihordlem6  41659  dihordlem7  41660  dihordlem7b  41661  dihord1  41664  dihord2a  41665  dihord11c  41670  dihord2pre  41671  dihord2pre2  41672  dihlsscpre  41680  dihord4  41704  dihord6b  41706  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetcN  41748  dihmeetbclemN  41750  dihmeetlem3N  41751  dihmeetlem9N  41761  dihmeetlem13N  41765  dihmeetlem20N  41772  mapdpglem24  42150  mapdpglem32  42151  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  mapdh9aOLDN  42236  hdmap14lem6  42319  sn-addlid  42836  mzpmfp  43179  mzpsubst  43180  pellexlem5  43261  pell14qrexpclnn0  43294  pellfundex  43314  qirropth  43336  monotuz  43369  congmul  43395  congsub  43398  mzpcong  43400  fzmaxdif  43409  jm2.15nn0  43431  idomsubgmo  43621  trclimalb2  44153  mnringmulrcld  44655  fourierdlem42  46577  fourierdlem48  46582  fourierdlem80  46614  prmdvdsfmtnof1lem1  48047  cycldlenngric  48404  gpgedgvtx1  48538  lidldomn1  48707  rngccatidALTV  48748  ringccatidALTV  48782  coe1sclmulval  48861  line2  49228  line2xlem  49229  line2x  49230  line2y  49231  itsclc0yqsol  49240  seposep  49401  iscnrm3rlem8  49422  iscnrm3llem2  49425