Theorem simp2r 1213

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simp12r  1300  simp22r  1306  simp32r  1312  fsnunf  7165  f1oiso2  7332  fnsuppres  8166  frrlem4  8265  omeulem2  8547  uniinqs  8774  unxpdomlem3  9198  sup0  9410  fin23lem11  10271  reclem3pr  11004  dedekind  11343  addlid  11363  subaddmulsub  11647  dmdcan  11898  nnadddir  12266  xaddass2  13250  xlt2add  13260  xadddi2  13297  expaddzlem  14115  expaddz  14116  expmulz  14118  expdiv  14123  expmordi  14177  pfxeq  14706  ccatopth2  14727  relexpaddnn  15061  o1add  15624  o1mul  15625  o1sub  15626  ntrivcvgmul  15915  prmexpb  16737  pcpremul  16862  pcdiv  16871  pcqmul  16872  pcqdiv  16876  4sqlem12  16975  f1ocpbllem  17537  ercpbl  17562  erlecpbl  17563  latjlej12  18470  latmlem12  18486  latj4  18504  gsumsgrpccat  18857  symgsssg  19490  symgfisg  19491  mndodcong  19565  cmn4  19824  ablsub4  19833  abladdsub4  19834  lsm4  19883  abvdom  20859  abvtrivd  20861  orngmul  20894  lspsnvs  21164  lspsneu  21173  lspfixed  21178  lspexch  21179  lsmcv  21191  lspsolvlem  21192  mvrf1  22017  coe1sclmulfv  22326  m1detdiag  22637  cnprest  23329  isreg2  23417  elptr  23613  hausflimlem  24019  trcfilu  24333  ssblps  24462  ssbl  24463  prdsxmslem2  24569  tgqioo  24840  metnrm  24903  bndth  25000  ncvspi  25198  cph2ass  25255  iscau3  25320  ovolunlem2  25540  dvres2  25954  dvfsumlem2  26069  dvfsum2  26076  deg1tm  26159  plyadd  26257  plymul  26258  coeeu  26265  coemullem  26290  aalioulem4  26376  cxplea  26738  cxple2  26739  cxplt2  26740  cxple2a  26741  cxpcn3lem  26789  angcan  26844  ang180lem5  26855  divsqrtsumlem  27021  logexprlim  27266  dchrvmasumlema  27541  dchrisum0lema  27555  logdivsum  27574  log2sumbnd  27585  padicabv  27671  nolesgn2ores  27713  nogesgn1o  27714  nogesgn1ores  27715  nolt02o  27736  nogt01o  27737  nosupinfsep  27773  noetalem1  27782  noeta2  27831  cutbdaylt  27868  expsgt0  28507  bdayfinbndlem1  28537  tghilberti2  28784  brbtwn2  29052  axcontlem4  29114  axcontlem8  29118  clwlkl1loop  29929  chscllem4  31789  mdslmd4i  32482  nexple  32996  measxun2  34468  measun  34469  mbfmco2  34523  probun  34677  satfv1fvfmla1  35737  wsuclem  36137  cgrcomim  36303  cgrcoml  36310  cgrcomr  36311  cgrdegen  36318  btwnintr  36333  btwnexch3  36334  btwnouttr  36338  btwnexch  36339  btwndiff  36341  ifscgr  36358  lineid  36397  btwnconn1lem7  36407  btwnconn1lem8  36408  btwnconn1lem9  36409  btwnconn1lem12  36412  midofsegid  36418  brsegle2  36423  btwnoutside  36439  outsideoftr  36443  ttcmin  36820  cnres2  38226  heibor  38284  lsmsat  39596  lkrlsp  39690  lkrlsp2  39691  lkrlsp3  39692  lshpkrlem6  39703  latm4  39821  omlspjN  39849  hlatj4  39962  4noncolr3  40041  4noncolr2  40042  4noncolr1  40043  3dimlem3a  40048  3dimlem4a  40051  3dimlem4  40052  3dimlem4OLDN  40053  1cvratex  40061  hlatexch4  40069  3atlem4  40074  atcvrlln2  40107  atcvrlln  40108  llnmlplnN  40127  lplnnlelln  40131  lvoli2  40169  lvolnlelln  40172  lvolnlelpln  40173  4atlem11b  40196  4atlem12b  40199  2lplnj  40208  dalemzeo  40221  dath2  40325  lncvrat  40370  cdlemb  40382  elpaddri  40390  padd4N  40428  llnmod2i2  40451  llnexchb2  40457  dalawlem1  40459  dalawlem2  40460  osumcllem6N  40549  pexmidlem3N  40560  pexmidlem4N  40561  lhp2lt  40589  lhp2at0  40620  lhp2atne  40622  lhp2at0ne  40624  lhpmod2i2  40626  lhpmod6i1  40627  lhpat  40631  lhpat3  40634  4atexlemex6  40662  ltrncoval  40733  ltrncnv  40734  ltrnnidn  40762  cdlemd7  40792  cdleme0b  40800  cdleme0c  40801  cdleme0fN  40806  cdleme0ex1N  40811  cdleme7d  40834  cdleme7e  40835  cdleme7ga  40836  cdleme7  40837  cdleme11a  40848  cdleme17c  40876  cdleme22gb  40882  cdlemeda  40886  cdleme20k  40907  cdleme21a  40913  cdleme21at  40916  cdleme21d  40918  cdleme22f2  40935  cdleme22g  40936  cdleme24  40940  cdleme28  40961  cdlemefrs29cpre1  40986  cdlemefr29exN  40990  cdlemefr32sn2aw  40992  cdleme32fva  41025  cdleme32fva1  41026  cdleme35a  41036  cdleme42c  41060  cdleme42e  41067  cdleme42f  41068  cdleme42g  41069  cdleme42h  41070  cdleme43bN  41078  cdleme46f2g2  41081  cdleme17d2  41083  cdleme4gfv  41095  cdlemeg46c  41101  cdlemeg46nlpq  41105  cdlemeg46gfre  41120  cdlemeg49lebilem  41127  cdleme50trn1  41137  cdleme50trn2  41139  cdleme50ltrn  41145  cdleme  41148  cdlemf1  41149  cdlemf  41151  trlord  41157  ltrniotavalbN  41172  cdlemg1cex  41176  cdlemg2dN  41178  cdlemg2ce  41180  cdlemg2fvlem  41182  cdlemg2idN  41184  cdlemg2kq  41190  cdlemg2l  41191  cdlemg7fvN  41212  cdlemg7aN  41213  cdlemg8a  41215  cdlemg11aq  41226  cdlemg12d  41234  cdlemg13a  41239  cdlemg13  41240  cdlemg14f  41241  cdlemg14g  41242  cdlemg17b  41250  cdlemg27a  41280  cdlemg31b0N  41282  cdlemg31a  41285  cdlemg31b  41286  cdlemg31c  41287  ltrnco  41307  trlcoabs2N  41310  trlcocnvat  41312  trlconid  41313  trlcolem  41314  cdlemg42  41317  cdlemg43  41318  cdlemg47a  41322  cdlemg46  41323  cdlemg47  41324  tendoeq1  41352  tendocoval  41354  tendoco2  41356  tendoplco2  41367  tendopltp  41368  cdlemh1  41403  cdlemh2  41404  cdlemi1  41406  cdlemi  41408  cdlemk1  41419  cdlemk2  41420  cdlemk3  41421  cdlemk4  41422  cdlemk8  41426  cdlemk9  41427  cdlemk9bN  41428  cdlemk31  41484  cdlemk28-3  41496  cdlemk19xlem  41530  cdlemk39u  41556  cdlemk19u  41558  cdlemk56w  41561  cdlemn7  41791  cdlemn8  41792  cdlemn9  41793  dihordlem6  41801  dihordlem7  41802  dihordlem7b  41803  dihord1  41806  dihord2a  41807  dihord11c  41812  dihord2pre  41813  dihord2pre2  41814  dihlsscpre  41822  dihord4  41846  dihord6b  41848  dihmeetlem2N  41887  dihglbcpreN  41888  dihmeetcN  41890  dihmeetbclemN  41892  dihmeetlem3N  41893  dihmeetlem9N  41903  dihmeetlem13N  41907  dihmeetlem20N  41914  mapdpglem24  42292  mapdpglem32  42293  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  mapdh9aOLDN  42378  hdmap14lem6  42461  sn-addlid  42977  mzpmfp  43292  mzpsubst  43293  pellexlem5  43374  pell14qrexpclnn0  43407  pellfundex  43427  qirropth  43449  monotuz  43482  congmul  43508  congsub  43511  mzpcong  43513  fzmaxdif  43522  jm2.15nn0  43544  idomsubgmo  43734  trclimalb2  44266  mnringmulrcld  44768  fourierdlem42  46687  fourierdlem48  46692  fourierdlem80  46724  prmdvdsfmtnof1lem1  48157  cycldlenngric  48514  gpgedgvtx1  48648  lidldomn1  48817  rngccatidALTV  48858  ringccatidALTV  48892  coe1sclmulval  48971  line2  49338  line2xlem  49339  line2x  49340  line2y  49341  itsclc0yqsol  49350  seposep  49511  iscnrm3rlem8  49532  iscnrm3llem2  49535