Theorem simp2r 1088

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl2r  1115  simpr2r  1121  simp12r  1175  simp22r  1181  simp32r  1187  funprgOLD  5941  fsnunf  6451  f1oiso2  6602  fnsuppres  7322  omeulem2  7663  uniinqs  7827  unxpdomlem3  8166  sup0  8372  fin23lem11  9139  reclem3pr  9871  dedekind  10200  addid2  10219  dmdcan  10735  xaddass2  12080  xlt2add  12090  xadddi2  12127  expaddzlem  12903  expaddz  12904  expmulz  12906  expdiv  12911  ccatopth2  13471  relexpaddnn  13791  o1add  14344  o1mul  14345  o1sub  14346  ntrivcvgmul  14634  prmexpb  15430  pcpremul  15548  pcdiv  15557  pcqmul  15558  pcqdiv  15562  4sqlem12  15660  f1ocpbllem  16184  ercpbl  16209  erlecpbl  16210  latjlej12  17067  latmlem12  17083  latj4  17101  symgsssg  17887  symgfisg  17888  mndodcong  17961  cmn4  18212  ablsub4  18218  abladdsub4  18219  lsm4  18263  abvdom  18838  abvtrivd  18840  lspsnvs  19114  lspsneu  19123  lspfixed  19128  lspexch  19129  lsmcv  19141  lspsolvlem  19142  mvrf1  19425  coe1sclmulfv  19653  m1detdiag  20403  cnprest  21093  isreg2  21181  elptr  21376  hausflimlem  21783  trcfilu  22098  ssblps  22227  ssbl  22228  prdsxmslem2  22334  tgqioo  22603  metnrm  22665  bndth  22757  ncvspi  22956  cph2ass  23013  iscau3  23076  ovolunlem2  23266  dvres2  23676  dvfsumlem2  23790  dvfsum2  23797  deg1tm  23878  plyadd  23973  plymul  23974  coeeu  23981  coemullem  24006  aalioulem4  24090  cxplea  24442  cxple2  24443  cxplt2  24444  cxple2a  24445  cxpcn3lem  24488  angcan  24532  ang180lem5  24543  divsqrtsumlem  24706  logexprlim  24950  dchrvmasumlema  25189  dchrisum0lema  25203  logdivsum  25222  log2sumbnd  25233  padicabv  25319  tghilberti2  25533  brbtwn2  25785  axcontlem4  25847  axcontlem8  25851  clwlkl1loop  26678  numclwwlkovf2exlem2  27212  chscllem4  28499  mdslmd4i  29192  orngmul  29803  nexple  30071  measxun2  30273  measun  30274  mbfmco2  30327  probun  30481  wsuclem  31773  wsuclemOLD  31774  nolesgn2ores  31825  nolt02o  31845  noetalem5  31867  scutbdaylt  31922  cgrcomim  32096  cgrcoml  32103  cgrcomr  32104  cgrdegen  32111  btwnintr  32126  btwnexch3  32127  btwnouttr  32131  btwnexch  32132  btwndiff  32134  ifscgr  32151  lineid  32190  btwnconn1lem7  32200  btwnconn1lem8  32201  btwnconn1lem9  32202  btwnconn1lem12  32205  midofsegid  32211  brsegle2  32216  btwnoutside  32232  outsideoftr  32236  cnres2  33562  heibor  33620  lsmsat  34295  lkrlsp  34389  lkrlsp2  34390  lkrlsp3  34391  lshpkrlem6  34402  latm4  34520  omlspjN  34548  hlatj4  34660  4noncolr3  34739  4noncolr2  34740  4noncolr1  34741  3dimlem3a  34746  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  1cvratex  34759  hlatexch4  34767  3atlem4  34772  atcvrlln2  34805  atcvrlln  34806  llnmlplnN  34825  lplnnlelln  34829  lvoli2  34867  lvolnlelln  34870  lvolnlelpln  34871  4atlem11b  34894  4atlem12b  34897  2lplnj  34906  dalemzeo  34919  dath2  35023  lncvrat  35068  cdlemb  35080  elpaddri  35088  padd4N  35126  llnmod2i2  35149  llnexchb2  35155  dalawlem1  35157  dalawlem2  35158  osumcllem6N  35247  pexmidlem3N  35258  pexmidlem4N  35259  lhp2lt  35287  lhp2at0  35318  lhp2atne  35320  lhp2at0ne  35322  lhpmod2i2  35324  lhpmod6i1  35325  lhpat  35329  lhpat3  35332  4atexlemex6  35360  ltrncoval  35431  ltrncnv  35432  ltrnnidn  35461  cdlemd7  35491  cdleme0b  35499  cdleme0c  35500  cdleme0fN  35505  cdleme0ex1N  35510  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme11a  35547  cdleme17c  35575  cdleme22gb  35581  cdlemeda  35585  cdleme20k  35607  cdleme21a  35613  cdleme21at  35616  cdleme21d  35618  cdleme22f2  35635  cdleme22g  35636  cdleme24  35640  cdleme28  35661  cdlemefrs29cpre1  35686  cdlemefr29exN  35690  cdlemefr32sn2aw  35692  cdleme32fva  35725  cdleme32fva1  35726  cdleme35a  35736  cdleme42c  35760  cdleme42e  35767  cdleme42f  35768  cdleme42g  35769  cdleme42h  35770  cdleme43bN  35778  cdleme46f2g2  35781  cdleme17d2  35783  cdleme4gfv  35795  cdlemeg46c  35801  cdlemeg46nlpq  35805  cdlemeg46gfre  35820  cdlemeg49lebilem  35827  cdleme50trn1  35837  cdleme50trn2  35839  cdleme50ltrn  35845  cdleme  35848  cdlemf1  35849  cdlemf  35851  trlord  35857  ltrniotavalbN  35872  cdlemg1cex  35876  cdlemg2dN  35878  cdlemg2ce  35880  cdlemg2fvlem  35882  cdlemg2idN  35884  cdlemg2kq  35890  cdlemg2l  35891  cdlemg7fvN  35912  cdlemg7aN  35913  cdlemg8a  35915  cdlemg11aq  35926  cdlemg12d  35934  cdlemg13a  35939  cdlemg13  35940  cdlemg14f  35941  cdlemg14g  35942  cdlemg17b  35950  cdlemg27a  35980  cdlemg31b0N  35982  cdlemg31a  35985  cdlemg31b  35986  cdlemg31c  35987  ltrnco  36007  trlcoabs2N  36010  trlcocnvat  36012  trlconid  36013  trlcolem  36014  cdlemg42  36017  cdlemg43  36018  cdlemg47a  36022  cdlemg46  36023  cdlemg47  36024  tendoeq1  36052  tendocoval  36054  tendoco2  36056  tendoplco2  36067  tendopltp  36068  cdlemh1  36103  cdlemh2  36104  cdlemi1  36106  cdlemi  36108  cdlemk1  36119  cdlemk2  36120  cdlemk3  36121  cdlemk4  36122  cdlemk8  36126  cdlemk9  36127  cdlemk9bN  36128  cdlemk31  36184  cdlemk28-3  36196  cdlemk19xlem  36230  cdlemk39u  36256  cdlemk19u  36258  cdlemk56w  36261  cdlemn7  36492  cdlemn8  36493  cdlemn9  36494  dihordlem6  36502  dihordlem7  36503  dihordlem7b  36504  dihord1  36507  dihord2a  36508  dihord11c  36513  dihord2pre  36514  dihord2pre2  36515  dihlsscpre  36523  dihord4  36547  dihord6b  36549  dihmeetlem2N  36588  dihglbcpreN  36589  dihmeetcN  36591  dihmeetbclemN  36593  dihmeetlem3N  36594  dihmeetlem9N  36604  dihmeetlem13N  36608  dihmeetlem20N  36615  mapdpglem24  36993  mapdpglem32  36994  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  mapdh9aOLDN  37080  hdmap14lem6  37165  mzpmfp  37310  mzpsubst  37311  pellexlem5  37397  pell14qrexpclnn0  37430  pellfundex  37450  qirropth  37473  monotuz  37506  expmordi  37512  congmul  37534  congsub  37537  mzpcong  37539  fzmaxdif  37548  jm2.15nn0  37570  idomsubgmo  37776  trclimalb2  38018  fourierdlem42  40366  fourierdlem48  40371  fourierdlem80  40403  prmdvdsfmtnof1lem1  41496  lidldomn1  41921  rngccatidALTV  41989  ringccatidALTV  42052  coe1sclmulval  42173