Theorem simp2r 1219

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp12r  1306  simp22r  1312  simp32r  1318  fsnunf  7191  f1resrcmplf1d  7280  f1oiso2  7361  fnsuppres  8212  frrlem4  8311  omeulem2  8595  uniinqs  8822  unxpdomlem3  9253  sup0  9463  fin23lem11  10399  reclem3pr  11138  dedekind  11477  addlid  11497  subaddmulsub  11783  dmdcan  12031  nnadddir  12398  xaddass2  13384  xlt2add  13394  xadddi2  13431  expaddzlem  14252  expaddz  14253  expmulz  14255  expdiv  14260  expmordi  14314  pfxeq  14850  ccatopth2  14871  relexpaddnn  15210  o1add  15787  o1mul  15788  o1sub  15789  ntrivcvgmul  16077  prmexpb  16901  pcpremul  17027  pcdiv  17036  pcqmul  17037  pcqdiv  17041  4sqlem12  17140  f1ocpbllem  17702  ercpbl  17727  erlecpbl  17728  latjlej12  18635  latmlem12  18651  latj4  18669  gsumsgrpccat  19042  symgsssg  19687  symgfisg  19688  mndodcong  19762  cmn4  20021  ablsub4  20030  abladdsub4  20031  lsm4  20080  abvdom  21093  abvtrivd  21095  orngmul  21128  lspsnvs  21398  lspsneu  21407  lspfixed  21412  lspexch  21413  lsmcv  21425  lspsolvlem  21426  mvrf1  22299  coe1sclmulfv  22608  m1detdiag  22918  cnprest  23613  isreg2  23701  elptr  23898  hausflimlem  24304  trcfilu  24618  ssblps  24747  ssbl  24748  prdsxmslem2  24854  tgqioo  25125  metnrm  25188  bndth  25285  ncvspi  25483  cph2ass  25540  iscau3  25605  ovolunlem2  25825  dvres2  26238  dvfsumlem2  26353  dvfsum2  26360  deg1tm  26443  plyadd  26542  plymul  26543  coeeu  26550  coemullem  26575  aalioulem4  26668  cxplea  27030  cxple2  27031  cxplt2  27032  cxple2a  27033  cxpcn3lem  27081  angcan  27136  ang180lem5  27147  divsqrtsumlem  27313  logexprlim  27558  dchrvmasumlema  27833  dchrisum0lema  27847  logdivsum  27866  log2sumbnd  27877  padicabv  27963  nolesgn2ores  28035  nogesgn1o  28036  nogesgn1ores  28037  nolt02o  28058  nogt01o  28059  nosupinfsep  28095  noetalem1  28104  noeta2  28153  cutbdaylt  28190  expsgt0  28829  bdayfinbndlem1  28859  tghilberti2  29112  brbtwn2  29489  axcontlem4  29551  axcontlem8  29555  clwlkl1loop  30376  umgr2cycllem  30752  chscllem4  32248  mdslmd4i  32941  nexple  33471  measxun2  34890  measun  34891  mbfmco2  34944  probun  35098  satfv1fvfmla1  36275  wsuclem  36680  cgrcomim  36847  cgrcoml  36854  cgrcomr  36855  cgrdegen  36862  btwnintr  36877  btwnexch3  36878  btwnouttr  36882  btwnexch  36883  btwndiff  36885  ifscgr  36902  lineid  36941  btwnconn1lem7  36951  btwnconn1lem8  36952  btwnconn1lem9  36953  btwnconn1lem12  36956  midofsegid  36962  brsegle2  36967  btwnoutside  36983  outsideoftr  36987  ttcmin  37377  cnres2  38791  heibor  38849  lsmsat  40159  lkrlsp  40253  lkrlsp2  40254  lkrlsp3  40255  lshpkrlem6  40266  latm4  40384  omlspjN  40412  hlatj4  40525  4noncolr3  40604  4noncolr2  40605  4noncolr1  40606  3dimlem3a  40611  3dimlem4a  40614  3dimlem4  40615  3dimlem4OLDN  40616  1cvratex  40624  hlatexch4  40632  3atlem4  40637  atcvrlln2  40670  atcvrlln  40671  llnmlplnN  40690  lplnnlelln  40694  lvoli2  40732  lvolnlelln  40735  lvolnlelpln  40736  4atlem11b  40759  4atlem12b  40762  2lplnj  40771  dalemzeo  40784  dath2  40888  lncvrat  40933  cdlemb  40945  elpaddri  40953  padd4N  40991  llnmod2i2  41014  llnexchb2  41020  dalawlem1  41022  dalawlem2  41023  osumcllem6N  41112  pexmidlem3N  41123  pexmidlem4N  41124  lhp2lt  41152  lhp2at0  41183  lhp2atne  41185  lhp2at0ne  41187  lhpmod2i2  41189  lhpmod6i1  41190  lhpat  41194  lhpat3  41197  4atexlemex6  41225  ltrncoval  41296  ltrncnv  41297  ltrnnidn  41325  cdlemd7  41355  cdleme0b  41363  cdleme0c  41364  cdleme0fN  41369  cdleme0ex1N  41374  cdleme7d  41397  cdleme7e  41398  cdleme7ga  41399  cdleme7  41400  cdleme11a  41411  cdleme17c  41439  cdleme22gb  41445  cdlemeda  41449  cdleme20k  41470  cdleme21a  41476  cdleme21at  41479  cdleme21d  41481  cdleme22f2  41498  cdleme22g  41499  cdleme24  41503  cdleme28  41524  cdlemefrs29cpre1  41549  cdlemefr29exN  41553  cdlemefr32sn2aw  41555  cdleme32fva  41588  cdleme32fva1  41589  cdleme35a  41599  cdleme42c  41623  cdleme42e  41630  cdleme42f  41631  cdleme42g  41632  cdleme42h  41633  cdleme43bN  41641  cdleme46f2g2  41644  cdleme17d2  41646  cdleme4gfv  41658  cdlemeg46c  41664  cdlemeg46nlpq  41668  cdlemeg46gfre  41683  cdlemeg49lebilem  41690  cdleme50trn1  41700  cdleme50trn2  41702  cdleme50ltrn  41708  cdleme  41711  cdlemf1  41712  cdlemf  41714  trlord  41720  ltrniotavalbN  41735  cdlemg1cex  41739  cdlemg2dN  41741  cdlemg2ce  41743  cdlemg2fvlem  41745  cdlemg2idN  41747  cdlemg2kq  41753  cdlemg2l  41754  cdlemg7fvN  41775  cdlemg7aN  41776  cdlemg8a  41778  cdlemg11aq  41789  cdlemg12d  41797  cdlemg13a  41802  cdlemg13  41803  cdlemg14f  41804  cdlemg14g  41805  cdlemg17b  41813  cdlemg27a  41843  cdlemg31b0N  41845  cdlemg31a  41848  cdlemg31b  41849  cdlemg31c  41850  ltrnco  41870  trlcoabs2N  41873  trlcocnvat  41875  trlconid  41876  trlcolem  41877  cdlemg42  41880  cdlemg43  41881  cdlemg47a  41885  cdlemg46  41886  cdlemg47  41887  tendoeq1  41915  tendocoval  41917  tendoco2  41919  tendoplco2  41930  tendopltp  41931  cdlemh1  41966  cdlemh2  41967  cdlemi1  41969  cdlemi  41971  cdlemk1  41982  cdlemk2  41983  cdlemk3  41984  cdlemk4  41985  cdlemk8  41989  cdlemk9  41990  cdlemk9bN  41991  cdlemk31  42047  cdlemk28-3  42059  cdlemk19xlem  42093  cdlemk39u  42119  cdlemk19u  42121  cdlemk56w  42124  cdlemn7  42354  cdlemn8  42355  cdlemn9  42356  dihordlem6  42364  dihordlem7  42365  dihordlem7b  42366  dihord1  42369  dihord2a  42370  dihord11c  42375  dihord2pre  42376  dihord2pre2  42377  dihlsscpre  42385  dihord4  42409  dihord6b  42411  dihmeetlem2N  42450  dihglbcpreN  42451  dihmeetcN  42453  dihmeetbclemN  42455  dihmeetlem3N  42456  dihmeetlem9N  42466  dihmeetlem13N  42470  dihmeetlem20N  42477  mapdpglem24  42855  mapdpglem32  42856  baerlem3lem2  42861  baerlem5alem2  42862  baerlem5blem2  42863  mapdh9aOLDN  42941  hdmap14lem6  43024  sn-addlid  43549  mzpmfp  43852  mzpsubst  43853  pellexlem5  43934  pell14qrexpclnn0  43967  pellfundex  43987  qirropth  44009  monotuz  44042  congmul  44068  congsub  44071  mzpcong  44073  fzmaxdif  44082  jm2.15nn0  44104  idomsubgmo  44289  trclimalb2  44820  mnringmulrcld  45320  fourierdlem42  47253  fourierdlem48  47258  fourierdlem80  47290  prmdvdsfmtnof1lem1  48763  cycldlenngric  49120  gpgedgvtx1  49254  lidldomn1  49422  rngccatidALTV  49463  ringccatidALTV  49497  coe1sclmulval  49591  line2  49958  line2xlem  49959  line2x  49960  itsclc0yqsol  49970  seposep  50134  iscnrm3rlem8  50155  iscnrm3llem2  50158