Theorem simp2r 1198

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp12r  1285  simp22r  1291  simp32r  1297  fsnunf  7194  f1oiso2  7360  fnsuppres  8196  frrlem4  8295  omeulem2  8604  uniinqs  8816  unxpdomlem3  9277  sup0  9490  fin23lem11  10341  reclem3pr  11073  dedekind  11408  addlid  11428  subaddmulsub  11708  dmdcan  11955  xaddass2  13262  xlt2add  13272  xadddi2  13309  expaddzlem  14103  expaddz  14104  expmulz  14106  expdiv  14111  expmordi  14164  pfxeq  14679  ccatopth2  14700  relexpaddnn  15031  o1add  15591  o1mul  15592  o1sub  15593  ntrivcvgmul  15881  prmexpb  16691  pcpremul  16812  pcdiv  16821  pcqmul  16822  pcqdiv  16826  4sqlem12  16925  f1ocpbllem  17506  ercpbl  17531  erlecpbl  17532  latjlej12  18447  latmlem12  18463  latj4  18481  gsumsgrpccat  18792  symgsssg  19422  symgfisg  19423  mndodcong  19497  cmn4  19756  ablsub4  19765  abladdsub4  19766  lsm4  19815  abvdom  20718  abvtrivd  20720  lspsnvs  21002  lspsneu  21011  lspfixed  21016  lspexch  21017  lsmcv  21029  lspsolvlem  21030  mvrf1  21928  coe1sclmulfv  22202  m1detdiag  22512  cnprest  23206  isreg2  23294  elptr  23490  hausflimlem  23896  trcfilu  24212  ssblps  24341  ssbl  24342  prdsxmslem2  24451  tgqioo  24729  metnrm  24791  bndth  24897  ncvspi  25097  cph2ass  25154  iscau3  25219  ovolunlem2  25440  dvres2  25854  dvfsumlem2  25974  dvfsumlem2OLD  25975  dvfsum2  25982  deg1tm  26067  plyadd  26164  plymul  26165  coeeu  26172  coemullem  26197  aalioulem4  26283  cxplea  26643  cxple2  26644  cxplt2  26645  cxple2a  26646  cxpcn3lem  26695  angcan  26747  ang180lem5  26758  divsqrtsumlem  26925  logexprlim  27171  dchrvmasumlema  27446  dchrisum0lema  27460  logdivsum  27479  log2sumbnd  27490  padicabv  27576  nolesgn2ores  27618  nogesgn1o  27619  nogesgn1ores  27620  nolt02o  27641  nogt01o  27642  nosupinfsep  27678  noetalem1  27687  noeta2  27730  scutbdaylt  27764  tghilberti2  28455  brbtwn2  28729  axcontlem4  28791  axcontlem8  28795  clwlkl1loop  29610  chscllem4  31463  mdslmd4i  32156  orngmul  33031  nexple  33628  measxun2  33829  measun  33830  mbfmco2  33885  probun  34039  satfv1fvfmla1  35033  wsuclem  35421  cgrcomim  35585  cgrcoml  35592  cgrcomr  35593  cgrdegen  35600  btwnintr  35615  btwnexch3  35616  btwnouttr  35620  btwnexch  35621  btwndiff  35623  ifscgr  35640  lineid  35679  btwnconn1lem7  35689  btwnconn1lem8  35690  btwnconn1lem9  35691  btwnconn1lem12  35694  midofsegid  35700  brsegle2  35705  btwnoutside  35721  outsideoftr  35725  cnres2  37236  heibor  37294  lsmsat  38480  lkrlsp  38574  lkrlsp2  38575  lkrlsp3  38576  lshpkrlem6  38587  latm4  38705  omlspjN  38733  hlatj4  38846  4noncolr3  38926  4noncolr2  38927  4noncolr1  38928  3dimlem3a  38933  3dimlem4a  38936  3dimlem4  38937  3dimlem4OLDN  38938  1cvratex  38946  hlatexch4  38954  3atlem4  38959  atcvrlln2  38992  atcvrlln  38993  llnmlplnN  39012  lplnnlelln  39016  lvoli2  39054  lvolnlelln  39057  lvolnlelpln  39058  4atlem11b  39081  4atlem12b  39084  2lplnj  39093  dalemzeo  39106  dath2  39210  lncvrat  39255  cdlemb  39267  elpaddri  39275  padd4N  39313  llnmod2i2  39336  llnexchb2  39342  dalawlem1  39344  dalawlem2  39345  osumcllem6N  39434  pexmidlem3N  39445  pexmidlem4N  39446  lhp2lt  39474  lhp2at0  39505  lhp2atne  39507  lhp2at0ne  39509  lhpmod2i2  39511  lhpmod6i1  39512  lhpat  39516  lhpat3  39519  4atexlemex6  39547  ltrncoval  39618  ltrncnv  39619  ltrnnidn  39647  cdlemd7  39677  cdleme0b  39685  cdleme0c  39686  cdleme0fN  39691  cdleme0ex1N  39696  cdleme7d  39719  cdleme7e  39720  cdleme7ga  39721  cdleme7  39722  cdleme11a  39733  cdleme17c  39761  cdleme22gb  39767  cdlemeda  39771  cdleme20k  39792  cdleme21a  39798  cdleme21at  39801  cdleme21d  39803  cdleme22f2  39820  cdleme22g  39821  cdleme24  39825  cdleme28  39846  cdlemefrs29cpre1  39871  cdlemefr29exN  39875  cdlemefr32sn2aw  39877  cdleme32fva  39910  cdleme32fva1  39911  cdleme35a  39921  cdleme42c  39945  cdleme42e  39952  cdleme42f  39953  cdleme42g  39954  cdleme42h  39955  cdleme43bN  39963  cdleme46f2g2  39966  cdleme17d2  39968  cdleme4gfv  39980  cdlemeg46c  39986  cdlemeg46nlpq  39990  cdlemeg46gfre  40005  cdlemeg49lebilem  40012  cdleme50trn1  40022  cdleme50trn2  40024  cdleme50ltrn  40030  cdleme  40033  cdlemf1  40034  cdlemf  40036  trlord  40042  ltrniotavalbN  40057  cdlemg1cex  40061  cdlemg2dN  40063  cdlemg2ce  40065  cdlemg2fvlem  40067  cdlemg2idN  40069  cdlemg2kq  40075  cdlemg2l  40076  cdlemg7fvN  40097  cdlemg7aN  40098  cdlemg8a  40100  cdlemg11aq  40111  cdlemg12d  40119  cdlemg13a  40124  cdlemg13  40125  cdlemg14f  40126  cdlemg14g  40127  cdlemg17b  40135  cdlemg27a  40165  cdlemg31b0N  40167  cdlemg31a  40170  cdlemg31b  40171  cdlemg31c  40172  ltrnco  40192  trlcoabs2N  40195  trlcocnvat  40197  trlconid  40198  trlcolem  40199  cdlemg42  40202  cdlemg43  40203  cdlemg47a  40207  cdlemg46  40208  cdlemg47  40209  tendoeq1  40237  tendocoval  40239  tendoco2  40241  tendoplco2  40252  tendopltp  40253  cdlemh1  40288  cdlemh2  40289  cdlemi1  40291  cdlemi  40293  cdlemk1  40304  cdlemk2  40305  cdlemk3  40306  cdlemk4  40307  cdlemk8  40311  cdlemk9  40312  cdlemk9bN  40313  cdlemk31  40369  cdlemk28-3  40381  cdlemk19xlem  40415  cdlemk39u  40441  cdlemk19u  40443  cdlemk56w  40446  cdlemn7  40676  cdlemn8  40677  cdlemn9  40678  dihordlem6  40686  dihordlem7  40687  dihordlem7b  40688  dihord1  40691  dihord2a  40692  dihord11c  40697  dihord2pre  40698  dihord2pre2  40699  dihlsscpre  40707  dihord4  40731  dihord6b  40733  dihmeetlem2N  40772  dihglbcpreN  40773  dihmeetcN  40775  dihmeetbclemN  40777  dihmeetlem3N  40778  dihmeetlem9N  40788  dihmeetlem13N  40792  dihmeetlem20N  40799  mapdpglem24  41177  mapdpglem32  41178  baerlem3lem2  41183  baerlem5alem2  41184  baerlem5blem2  41185  mapdh9aOLDN  41263  hdmap14lem6  41346  nnadddir  41845  sn-addlid  41959  mzpmfp  42167  mzpsubst  42168  pellexlem5  42253  pell14qrexpclnn0  42286  pellfundex  42306  qirropth  42328  monotuz  42362  congmul  42388  congsub  42391  mzpcong  42393  fzmaxdif  42402  jm2.15nn0  42424  idomsubgmo  42621  trclimalb2  43156  mnringmulrcld  43665  fourierdlem42  45537  fourierdlem48  45542  fourierdlem80  45574  prmdvdsfmtnof1lem1  46924  lidldomn1  47293  rngccatidALTV  47334  ringccatidALTV  47368  coe1sclmulval  47453  line2  47825  line2xlem  47826  line2x  47827  line2y  47828  itsclc0yqsol  47837  seposep  47944  iscnrm3rlem8  47966  iscnrm3llem2  47969