Theorem simp2r 1207

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 485	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1140	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simp12r  1294  simp22r  1300  simp32r  1306  fsnunf  7136  f1oiso2  7303  fnsuppres  8138  frrlem4  8236  omeulem2  8515  uniinqs  8741  unxpdomlem3  9165  sup0  9377  fin23lem11  10237  reclem3pr  10970  dedekind  11307  addlid  11327  subaddmulsub  11611  dmdcan  11863  nnadddir  12231  xaddass2  13200  xlt2add  13210  xadddi2  13247  expaddzlem  14065  expaddz  14066  expmulz  14068  expdiv  14073  expmordi  14127  pfxeq  14656  ccatopth2  14677  relexpaddnn  15011  o1add  15574  o1mul  15575  o1sub  15576  ntrivcvgmul  15865  prmexpb  16687  pcpremul  16812  pcdiv  16821  pcqmul  16822  pcqdiv  16826  4sqlem12  16925  f1ocpbllem  17486  ercpbl  17511  erlecpbl  17512  latjlej12  18419  latmlem12  18435  latj4  18453  gsumsgrpccat  18806  symgsssg  19440  symgfisg  19441  mndodcong  19515  cmn4  19774  ablsub4  19783  abladdsub4  19784  lsm4  19833  abvdom  20809  abvtrivd  20811  orngmul  20844  lspsnvs  21114  lspsneu  21123  lspfixed  21128  lspexch  21129  lsmcv  21141  lspsolvlem  21142  mvrf1  21967  coe1sclmulfv  22276  m1detdiag  22587  cnprest  23279  isreg2  23367  elptr  23563  hausflimlem  23969  trcfilu  24283  ssblps  24412  ssbl  24413  prdsxmslem2  24519  tgqioo  24790  metnrm  24853  bndth  24950  ncvspi  25148  cph2ass  25205  iscau3  25270  ovolunlem2  25490  dvres2  25904  dvfsumlem2  26019  dvfsum2  26026  deg1tm  26109  plyadd  26207  plymul  26208  coeeu  26215  coemullem  26240  aalioulem4  26326  cxplea  26685  cxple2  26686  cxplt2  26687  cxple2a  26688  cxpcn3lem  26736  angcan  26791  ang180lem5  26802  divsqrtsumlem  26968  logexprlim  27213  dchrvmasumlema  27488  dchrisum0lema  27502  logdivsum  27521  log2sumbnd  27532  padicabv  27618  nolesgn2ores  27661  nogesgn1o  27662  nogesgn1ores  27663  nolt02o  27684  nogt01o  27685  nosupinfsep  27721  noetalem1  27730  noeta2  27778  cutbdaylt  27815  expsgt0  28454  bdayfinbndlem1  28484  tghilberti2  28731  brbtwn2  28999  axcontlem4  29061  axcontlem8  29065  clwlkl1loop  29876  chscllem4  31736  mdslmd4i  32429  nexple  32943  measxun2  34401  measun  34402  mbfmco2  34456  probun  34610  satfv1fvfmla1  35658  wsuclem  36058  cgrcomim  36224  cgrcoml  36231  cgrcomr  36232  cgrdegen  36239  btwnintr  36254  btwnexch3  36255  btwnouttr  36259  btwnexch  36260  btwndiff  36262  ifscgr  36279  lineid  36318  btwnconn1lem7  36328  btwnconn1lem8  36329  btwnconn1lem9  36330  btwnconn1lem12  36333  midofsegid  36339  brsegle2  36344  btwnoutside  36360  outsideoftr  36364  ttcmin  36731  cnres2  38137  heibor  38195  lsmsat  39507  lkrlsp  39601  lkrlsp2  39602  lkrlsp3  39603  lshpkrlem6  39614  latm4  39732  omlspjN  39760  hlatj4  39873  4noncolr3  39952  4noncolr2  39953  4noncolr1  39954  3dimlem3a  39959  3dimlem4a  39962  3dimlem4  39963  3dimlem4OLDN  39964  1cvratex  39972  hlatexch4  39980  3atlem4  39985  atcvrlln2  40018  atcvrlln  40019  llnmlplnN  40038  lplnnlelln  40042  lvoli2  40080  lvolnlelln  40083  lvolnlelpln  40084  4atlem11b  40107  4atlem12b  40110  2lplnj  40119  dalemzeo  40132  dath2  40236  lncvrat  40281  cdlemb  40293  elpaddri  40301  padd4N  40339  llnmod2i2  40362  llnexchb2  40368  dalawlem1  40370  dalawlem2  40371  osumcllem6N  40460  pexmidlem3N  40471  pexmidlem4N  40472  lhp2lt  40500  lhp2at0  40531  lhp2atne  40533  lhp2at0ne  40535  lhpmod2i2  40537  lhpmod6i1  40538  lhpat  40542  lhpat3  40545  4atexlemex6  40573  ltrncoval  40644  ltrncnv  40645  ltrnnidn  40673  cdlemd7  40703  cdleme0b  40711  cdleme0c  40712  cdleme0fN  40717  cdleme0ex1N  40722  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme11a  40759  cdleme17c  40787  cdleme22gb  40793  cdlemeda  40797  cdleme20k  40818  cdleme21a  40824  cdleme21at  40827  cdleme21d  40829  cdleme22f2  40846  cdleme22g  40847  cdleme24  40851  cdleme28  40872  cdlemefrs29cpre1  40897  cdlemefr29exN  40901  cdlemefr32sn2aw  40903  cdleme32fva  40936  cdleme32fva1  40937  cdleme35a  40947  cdleme42c  40971  cdleme42e  40978  cdleme42f  40979  cdleme42g  40980  cdleme42h  40981  cdleme43bN  40989  cdleme46f2g2  40992  cdleme17d2  40994  cdleme4gfv  41006  cdlemeg46c  41012  cdlemeg46nlpq  41016  cdlemeg46gfre  41031  cdlemeg49lebilem  41038  cdleme50trn1  41048  cdleme50trn2  41050  cdleme50ltrn  41056  cdleme  41059  cdlemf1  41060  cdlemf  41062  trlord  41068  ltrniotavalbN  41083  cdlemg1cex  41087  cdlemg2dN  41089  cdlemg2ce  41091  cdlemg2fvlem  41093  cdlemg2idN  41095  cdlemg2kq  41101  cdlemg2l  41102  cdlemg7fvN  41123  cdlemg7aN  41124  cdlemg8a  41126  cdlemg11aq  41137  cdlemg12d  41145  cdlemg13a  41150  cdlemg13  41151  cdlemg14f  41152  cdlemg14g  41153  cdlemg17b  41161  cdlemg27a  41191  cdlemg31b0N  41193  cdlemg31a  41196  cdlemg31b  41197  cdlemg31c  41198  ltrnco  41218  trlcoabs2N  41221  trlcocnvat  41223  trlconid  41224  trlcolem  41225  cdlemg42  41228  cdlemg43  41229  cdlemg47a  41233  cdlemg46  41234  cdlemg47  41235  tendoeq1  41263  tendocoval  41265  tendoco2  41267  tendoplco2  41278  tendopltp  41279  cdlemh1  41314  cdlemh2  41315  cdlemi1  41317  cdlemi  41319  cdlemk1  41330  cdlemk2  41331  cdlemk3  41332  cdlemk4  41333  cdlemk8  41337  cdlemk9  41338  cdlemk9bN  41339  cdlemk31  41395  cdlemk28-3  41407  cdlemk19xlem  41441  cdlemk39u  41467  cdlemk19u  41469  cdlemk56w  41472  cdlemn7  41702  cdlemn8  41703  cdlemn9  41704  dihordlem6  41712  dihordlem7  41713  dihordlem7b  41714  dihord1  41717  dihord2a  41718  dihord11c  41723  dihord2pre  41724  dihord2pre2  41725  dihlsscpre  41733  dihord4  41757  dihord6b  41759  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetcN  41801  dihmeetbclemN  41803  dihmeetlem3N  41804  dihmeetlem9N  41814  dihmeetlem13N  41818  dihmeetlem20N  41825  mapdpglem24  42203  mapdpglem32  42204  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  mapdh9aOLDN  42289  hdmap14lem6  42372  sn-addlid  42888  mzpmfp  43203  mzpsubst  43204  pellexlem5  43285  pell14qrexpclnn0  43318  pellfundex  43338  qirropth  43360  monotuz  43393  congmul  43419  congsub  43422  mzpcong  43424  fzmaxdif  43433  jm2.15nn0  43455  idomsubgmo  43645  trclimalb2  44177  mnringmulrcld  44679  fourierdlem42  46599  fourierdlem48  46604  fourierdlem80  46636  prmdvdsfmtnof1lem1  48069  cycldlenngric  48426  gpgedgvtx1  48560  lidldomn1  48729  rngccatidALTV  48770  ringccatidALTV  48804  coe1sclmulval  48883  line2  49250  line2xlem  49251  line2x  49252  line2y  49253  itsclc0yqsol  49262  seposep  49423  iscnrm3rlem8  49444  iscnrm3llem2  49447