Theorem simp2r 1191

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 1125	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

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

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 1080

This theorem is referenced by:  simp12r  1278  simp22r  1284  simp32r  1290  fsnunf  6805  f1oiso2  6959  fnsuppres  7699  omeulem2  8050  uniinqs  8218  unxpdomlem3  8560  sup0  8766  fin23lem11  9574  reclem3pr  10306  dedekind  10639  addid2  10659  subaddmulsub  10940  dmdcan  11187  xaddass2  12482  xlt2add  12492  xadddi2  12529  expaddzlem  13310  expaddz  13311  expmulz  13313  expdiv  13318  expmordi  13369  ccatopth2  13903  relexpaddnn  14232  o1add  14792  o1mul  14793  o1sub  14794  ntrivcvgmul  15079  prmexpb  15879  pcpremul  15997  pcdiv  16006  pcqmul  16007  pcqdiv  16011  4sqlem12  16109  f1ocpbllem  16614  ercpbl  16639  erlecpbl  16640  latjlej12  17494  latmlem12  17510  latj4  17528  symgsssg  18314  symgfisg  18315  mndodcong  18389  cmn4  18640  ablsub4  18646  abladdsub4  18647  lsm4  18691  abvdom  19287  abvtrivd  19289  lspsnvs  19564  lspsneu  19573  lspfixed  19578  lspexch  19579  lsmcv  19591  lspsolvlem  19592  mvrf1  19881  coe1sclmulfv  20122  m1detdiag  20878  cnprest  21569  isreg2  21657  elptr  21853  hausflimlem  22259  trcfilu  22574  ssblps  22703  ssbl  22704  prdsxmslem2  22810  tgqioo  23079  metnrm  23141  bndth  23233  ncvspi  23431  cph2ass  23488  iscau3  23552  ovolunlem2  23770  dvres2  24181  dvfsumlem2  24295  dvfsum2  24302  deg1tm  24383  plyadd  24478  plymul  24479  coeeu  24486  coemullem  24511  aalioulem4  24595  cxplea  24948  cxple2  24949  cxplt2  24950  cxple2a  24951  cxpcn3lem  24997  angcan  25049  ang180lem5  25060  divsqrtsumlem  25227  logexprlim  25471  dchrvmasumlema  25746  dchrisum0lema  25760  logdivsum  25779  log2sumbnd  25790  padicabv  25876  tghilberti2  26094  brbtwn2  26362  axcontlem4  26424  axcontlem8  26428  clwlkl1loop  27239  clwwlknonex2lem2  27562  chscllem4  29096  mdslmd4i  29789  orngmul  30485  nexple  30841  measxun2  31042  measun  31043  mbfmco2  31096  probun  31250  wsuclem  32666  frrlem4  32680  nolesgn2ores  32733  nolt02o  32753  noetalem5  32775  scutbdaylt  32830  cgrcomim  33004  cgrcoml  33011  cgrcomr  33012  cgrdegen  33019  btwnintr  33034  btwnexch3  33035  btwnouttr  33039  btwnexch  33040  btwndiff  33042  ifscgr  33059  lineid  33098  btwnconn1lem7  33108  btwnconn1lem8  33109  btwnconn1lem9  33110  btwnconn1lem12  33113  midofsegid  33119  brsegle2  33124  btwnoutside  33140  outsideoftr  33144  cnres2  34519  heibor  34577  lsmsat  35625  lkrlsp  35719  lkrlsp2  35720  lkrlsp3  35721  lshpkrlem6  35732  latm4  35850  omlspjN  35878  hlatj4  35991  4noncolr3  36070  4noncolr2  36071  4noncolr1  36072  3dimlem3a  36077  3dimlem4a  36080  3dimlem4  36081  3dimlem4OLDN  36082  1cvratex  36090  hlatexch4  36098  3atlem4  36103  atcvrlln2  36136  atcvrlln  36137  llnmlplnN  36156  lplnnlelln  36160  lvoli2  36198  lvolnlelln  36201  lvolnlelpln  36202  4atlem11b  36225  4atlem12b  36228  2lplnj  36237  dalemzeo  36250  dath2  36354  lncvrat  36399  cdlemb  36411  elpaddri  36419  padd4N  36457  llnmod2i2  36480  llnexchb2  36486  dalawlem1  36488  dalawlem2  36489  osumcllem6N  36578  pexmidlem3N  36589  pexmidlem4N  36590  lhp2lt  36618  lhp2at0  36649  lhp2atne  36651  lhp2at0ne  36653  lhpmod2i2  36655  lhpmod6i1  36656  lhpat  36660  lhpat3  36663  4atexlemex6  36691  ltrncoval  36762  ltrncnv  36763  ltrnnidn  36791  cdlemd7  36821  cdleme0b  36829  cdleme0c  36830  cdleme0fN  36835  cdleme0ex1N  36840  cdleme7d  36863  cdleme7e  36864  cdleme7ga  36865  cdleme7  36866  cdleme11a  36877  cdleme17c  36905  cdleme22gb  36911  cdlemeda  36915  cdleme20k  36936  cdleme21a  36942  cdleme21at  36945  cdleme21d  36947  cdleme22f2  36964  cdleme22g  36965  cdleme24  36969  cdleme28  36990  cdlemefrs29cpre1  37015  cdlemefr29exN  37019  cdlemefr32sn2aw  37021  cdleme32fva  37054  cdleme32fva1  37055  cdleme35a  37065  cdleme42c  37089  cdleme42e  37096  cdleme42f  37097  cdleme42g  37098  cdleme42h  37099  cdleme43bN  37107  cdleme46f2g2  37110  cdleme17d2  37112  cdleme4gfv  37124  cdlemeg46c  37130  cdlemeg46nlpq  37134  cdlemeg46gfre  37149  cdlemeg49lebilem  37156  cdleme50trn1  37166  cdleme50trn2  37168  cdleme50ltrn  37174  cdleme  37177  cdlemf1  37178  cdlemf  37180  trlord  37186  ltrniotavalbN  37201  cdlemg1cex  37205  cdlemg2dN  37207  cdlemg2ce  37209  cdlemg2fvlem  37211  cdlemg2idN  37213  cdlemg2kq  37219  cdlemg2l  37220  cdlemg7fvN  37241  cdlemg7aN  37242  cdlemg8a  37244  cdlemg11aq  37255  cdlemg12d  37263  cdlemg13a  37268  cdlemg13  37269  cdlemg14f  37270  cdlemg14g  37271  cdlemg17b  37279  cdlemg27a  37309  cdlemg31b0N  37311  cdlemg31a  37314  cdlemg31b  37315  cdlemg31c  37316  ltrnco  37336  trlcoabs2N  37339  trlcocnvat  37341  trlconid  37342  trlcolem  37343  cdlemg42  37346  cdlemg43  37347  cdlemg47a  37351  cdlemg46  37352  cdlemg47  37353  tendoeq1  37381  tendocoval  37383  tendoco2  37385  tendoplco2  37396  tendopltp  37397  cdlemh1  37432  cdlemh2  37433  cdlemi1  37435  cdlemi  37437  cdlemk1  37448  cdlemk2  37449  cdlemk3  37450  cdlemk4  37451  cdlemk8  37455  cdlemk9  37456  cdlemk9bN  37457  cdlemk31  37513  cdlemk28-3  37525  cdlemk19xlem  37559  cdlemk39u  37585  cdlemk19u  37587  cdlemk56w  37590  cdlemn7  37820  cdlemn8  37821  cdlemn9  37822  dihordlem6  37830  dihordlem7  37831  dihordlem7b  37832  dihord1  37835  dihord2a  37836  dihord11c  37841  dihord2pre  37842  dihord2pre2  37843  dihlsscpre  37851  dihord4  37875  dihord6b  37877  dihmeetlem2N  37916  dihglbcpreN  37917  dihmeetcN  37919  dihmeetbclemN  37921  dihmeetlem3N  37922  dihmeetlem9N  37932  dihmeetlem13N  37936  dihmeetlem20N  37943  mapdpglem24  38321  mapdpglem32  38322  baerlem3lem2  38327  baerlem5alem2  38328  baerlem5blem2  38329  mapdh9aOLDN  38407  hdmap14lem6  38490  mzpmfp  38779  mzpsubst  38780  pellexlem5  38866  pell14qrexpclnn0  38899  pellfundex  38919  qirropth  38941  monotuz  38974  congmul  39000  congsub  39003  mzpcong  39005  fzmaxdif  39014  jm2.15nn0  39036  idomsubgmo  39234  trclimalb2  39507  fourierdlem42  41930  fourierdlem48  41935  fourierdlem80  41967  prmdvdsfmtnof1lem1  43182  lidldomn1  43624  rngccatidALTV  43692  ringccatidALTV  43755  coe1sclmulval  43873  line2  44174  line2xlem  44175  line2x  44176  line2y  44177  itsclc0yqsol  44186