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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simp12r  1289  simp22r  1295  simp32r  1301  fsnunf  7000  f1oiso2  7161  fnsuppres  7933  frrlem4  8030  omeulem2  8311  uniinqs  8479  unxpdomlem3  8884  sup0  9082  fin23lem11  9931  reclem3pr  10663  dedekind  10995  addid2  11015  subaddmulsub  11295  dmdcan  11542  xaddass2  12840  xlt2add  12850  xadddi2  12887  expaddzlem  13678  expaddz  13679  expmulz  13681  expdiv  13686  expmordi  13737  pfxeq  14261  ccatopth2  14282  relexpaddnn  14614  o1add  15175  o1mul  15176  o1sub  15177  ntrivcvgmul  15466  prmexpb  16277  pcpremul  16396  pcdiv  16405  pcqmul  16406  pcqdiv  16410  4sqlem12  16509  f1ocpbllem  17029  ercpbl  17054  erlecpbl  17055  latjlej12  17961  latmlem12  17977  latj4  17995  gsumsgrpccat  18266  symgsssg  18859  symgfisg  18860  mndodcong  18934  cmn4  19190  ablsub4  19198  abladdsub4  19199  lsm4  19245  abvdom  19874  abvtrivd  19876  lspsnvs  20151  lspsneu  20160  lspfixed  20165  lspexch  20166  lsmcv  20178  lspsolvlem  20179  mvrf1  20950  coe1sclmulfv  21204  m1detdiag  21494  cnprest  22186  isreg2  22274  elptr  22470  hausflimlem  22876  trcfilu  23191  ssblps  23320  ssbl  23321  prdsxmslem2  23427  tgqioo  23697  metnrm  23759  bndth  23855  ncvspi  24053  cph2ass  24110  iscau3  24175  ovolunlem2  24395  dvres2  24809  dvfsumlem2  24924  dvfsum2  24931  deg1tm  25016  plyadd  25111  plymul  25112  coeeu  25119  coemullem  25144  aalioulem4  25228  cxplea  25584  cxple2  25585  cxplt2  25586  cxple2a  25587  cxpcn3lem  25633  angcan  25685  ang180lem5  25696  divsqrtsumlem  25862  logexprlim  26106  dchrvmasumlema  26381  dchrisum0lema  26395  logdivsum  26414  log2sumbnd  26425  padicabv  26511  tghilberti2  26729  brbtwn2  26996  axcontlem4  27058  axcontlem8  27062  clwlkl1loop  27870  chscllem4  29721  mdslmd4i  30414  orngmul  31221  nexple  31689  measxun2  31890  measun  31891  mbfmco2  31944  probun  32098  satfv1fvfmla1  33098  wsuclem  33556  nolesgn2ores  33612  nogesgn1o  33613  nogesgn1ores  33614  nolt02o  33635  nogt01o  33636  nosupinfsep  33672  noetalem1  33681  noeta2  33716  scutbdaylt  33749  cgrcomim  34028  cgrcoml  34035  cgrcomr  34036  cgrdegen  34043  btwnintr  34058  btwnexch3  34059  btwnouttr  34063  btwnexch  34064  btwndiff  34066  ifscgr  34083  lineid  34122  btwnconn1lem7  34132  btwnconn1lem8  34133  btwnconn1lem9  34134  btwnconn1lem12  34137  midofsegid  34143  brsegle2  34148  btwnoutside  34164  outsideoftr  34168  cnres2  35658  heibor  35716  lsmsat  36759  lkrlsp  36853  lkrlsp2  36854  lkrlsp3  36855  lshpkrlem6  36866  latm4  36984  omlspjN  37012  hlatj4  37125  4noncolr3  37204  4noncolr2  37205  4noncolr1  37206  3dimlem3a  37211  3dimlem4a  37214  3dimlem4  37215  3dimlem4OLDN  37216  1cvratex  37224  hlatexch4  37232  3atlem4  37237  atcvrlln2  37270  atcvrlln  37271  llnmlplnN  37290  lplnnlelln  37294  lvoli2  37332  lvolnlelln  37335  lvolnlelpln  37336  4atlem11b  37359  4atlem12b  37362  2lplnj  37371  dalemzeo  37384  dath2  37488  lncvrat  37533  cdlemb  37545  elpaddri  37553  padd4N  37591  llnmod2i2  37614  llnexchb2  37620  dalawlem1  37622  dalawlem2  37623  osumcllem6N  37712  pexmidlem3N  37723  pexmidlem4N  37724  lhp2lt  37752  lhp2at0  37783  lhp2atne  37785  lhp2at0ne  37787  lhpmod2i2  37789  lhpmod6i1  37790  lhpat  37794  lhpat3  37797  4atexlemex6  37825  ltrncoval  37896  ltrncnv  37897  ltrnnidn  37925  cdlemd7  37955  cdleme0b  37963  cdleme0c  37964  cdleme0fN  37969  cdleme0ex1N  37974  cdleme7d  37997  cdleme7e  37998  cdleme7ga  37999  cdleme7  38000  cdleme11a  38011  cdleme17c  38039  cdleme22gb  38045  cdlemeda  38049  cdleme20k  38070  cdleme21a  38076  cdleme21at  38079  cdleme21d  38081  cdleme22f2  38098  cdleme22g  38099  cdleme24  38103  cdleme28  38124  cdlemefrs29cpre1  38149  cdlemefr29exN  38153  cdlemefr32sn2aw  38155  cdleme32fva  38188  cdleme32fva1  38189  cdleme35a  38199  cdleme42c  38223  cdleme42e  38230  cdleme42f  38231  cdleme42g  38232  cdleme42h  38233  cdleme43bN  38241  cdleme46f2g2  38244  cdleme17d2  38246  cdleme4gfv  38258  cdlemeg46c  38264  cdlemeg46nlpq  38268  cdlemeg46gfre  38283  cdlemeg49lebilem  38290  cdleme50trn1  38300  cdleme50trn2  38302  cdleme50ltrn  38308  cdleme  38311  cdlemf1  38312  cdlemf  38314  trlord  38320  ltrniotavalbN  38335  cdlemg1cex  38339  cdlemg2dN  38341  cdlemg2ce  38343  cdlemg2fvlem  38345  cdlemg2idN  38347  cdlemg2kq  38353  cdlemg2l  38354  cdlemg7fvN  38375  cdlemg7aN  38376  cdlemg8a  38378  cdlemg11aq  38389  cdlemg12d  38397  cdlemg13a  38402  cdlemg13  38403  cdlemg14f  38404  cdlemg14g  38405  cdlemg17b  38413  cdlemg27a  38443  cdlemg31b0N  38445  cdlemg31a  38448  cdlemg31b  38449  cdlemg31c  38450  ltrnco  38470  trlcoabs2N  38473  trlcocnvat  38475  trlconid  38476  trlcolem  38477  cdlemg42  38480  cdlemg43  38481  cdlemg47a  38485  cdlemg46  38486  cdlemg47  38487  tendoeq1  38515  tendocoval  38517  tendoco2  38519  tendoplco2  38530  tendopltp  38531  cdlemh1  38566  cdlemh2  38567  cdlemi1  38569  cdlemi  38571  cdlemk1  38582  cdlemk2  38583  cdlemk3  38584  cdlemk4  38585  cdlemk8  38589  cdlemk9  38590  cdlemk9bN  38591  cdlemk31  38647  cdlemk28-3  38659  cdlemk19xlem  38693  cdlemk39u  38719  cdlemk19u  38721  cdlemk56w  38724  cdlemn7  38954  cdlemn8  38955  cdlemn9  38956  dihordlem6  38964  dihordlem7  38965  dihordlem7b  38966  dihord1  38969  dihord2a  38970  dihord11c  38975  dihord2pre  38976  dihord2pre2  38977  dihlsscpre  38985  dihord4  39009  dihord6b  39011  dihmeetlem2N  39050  dihglbcpreN  39051  dihmeetcN  39053  dihmeetbclemN  39055  dihmeetlem3N  39056  dihmeetlem9N  39066  dihmeetlem13N  39070  dihmeetlem20N  39077  mapdpglem24  39455  mapdpglem32  39456  baerlem3lem2  39461  baerlem5alem2  39462  baerlem5blem2  39463  mapdh9aOLDN  39541  hdmap14lem6  39624  nnadddir  40007  sn-addid2  40095  mzpmfp  40272  mzpsubst  40273  pellexlem5  40358  pell14qrexpclnn0  40391  pellfundex  40411  qirropth  40433  monotuz  40466  congmul  40492  congsub  40495  mzpcong  40497  fzmaxdif  40506  jm2.15nn0  40528  idomsubgmo  40726  trclimalb2  41011  mnringmulrcld  41519  fourierdlem42  43365  fourierdlem48  43370  fourierdlem80  43402  prmdvdsfmtnof1lem1  44709  lidldomn1  45152  rngccatidALTV  45220  ringccatidALTV  45283  coe1sclmulval  45399  line2  45771  line2xlem  45772  line2x  45773  line2y  45774  itsclc0yqsol  45783  seposep  45892  iscnrm3rlem8  45914  iscnrm3llem2  45917