Theorem simp2l 1200

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2l	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1134	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simp12l  1287  simp22l  1293  simp32l  1299  fsnunf  7159  f1oiso2  7327  fpr3g  8264  omeulem2  8547  uniinqs  8770  unxpdomlem3  9199  gruina  10771  dedekind  11337  addlid  11357  subaddmulsub  11641  dmdcan  11892  xaddass  13209  xaddass2  13210  xlt2add  13220  xmulasslem3  13246  xadddi2  13257  xadddi2r  13258  expaddzlem  14070  expaddz  14071  expmulz  14073  expdiv  14078  expmordi  14132  modexp  14203  pfxeq  14661  ccatopth2  14682  swrdco  14803  o1add  15580  o1mul  15581  o1sub  15582  fsumsplitsnun  15721  ntrivcvgmul  15868  prmexpb  16689  pcpremul  16814  pcdiv  16823  pcqmul  16824  pcqdiv  16828  4sqlem12  16927  f1ocpbllem  17487  ercpbl  17512  erlecpbl  17513  latjlej12  18414  latmlem12  18430  latj4  18448  latj4rot  18449  gsumsgrpccat  18767  gsmsymgreqlem2  19361  symgsssg  19397  symgfisg  19398  mndodcong  19472  cmn4  19731  ablsub4  19740  abladdsub4  19741  lsm4  19790  abvdom  20739  abvres  20740  abvtrivd  20741  lspsnvs  21024  lspsneu  21033  lspfixed  21038  lspexch  21039  lsmcv  21051  lspsolvlem  21052  ring2idlqus1  21229  coe1sclmulfv  22169  matvscacell  22323  m1detdiag  22484  cramerimplem3  22572  cnprest  23176  hausnei2  23240  isreg2  23264  cmpcld  23289  llyrest  23372  nllyrest  23373  elptr  23460  basqtop  23598  hausflimlem  23866  tmdgsum  23982  utop2nei  24138  trcfilu  24181  ssblps  24310  ssbl  24311  prdsxmslem2  24417  tgqioo  24688  metnrm  24751  bndth  24857  ncvspi  25056  ncvs1  25057  cph2ass  25113  lmmbr2  25159  iscau3  25178  bcthlem5  25228  ovolunlem2  25399  dvres2  25813  dvfsumlem2  25933  dvfsumlem2OLD  25934  plyadd  26122  plymul  26123  coeeu  26130  coemullem  26155  aalioulem4  26243  mulcxp  26594  cxplea  26605  cxple2  26606  cxplt2  26607  cxpcn3lem  26657  angcan  26712  ang180lem5  26723  divsqrtsumlem  26890  logexprlim  27136  dchrvmasumlema  27411  dchrisum0lema  27425  logdivsum  27444  log2sumbnd  27455  abvcxp  27526  padicabv  27541  nolesgn2ores  27584  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem2  27621  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  noinffv  27633  noinfres  27634  noinfbnd1lem1  27635  noinfbnd1lem2  27636  noinfbnd1lem4  27638  noinfbnd1lem6  27640  nosupinfsep  27644  scutbdaylt  27730  expsgt0  28322  tghilberti2  28565  brbtwn2  28832  axcontlem4  28894  axcontlem8  28898  clwlkl1loop  29713  clwwlknonex2lem2  30037  clwlknon2num  30297  numclwlk1lem2  30299  chscllem4  31569  orngmul  33281  measxun2  34200  measun  34201  mbfmco2  34256  probun  34410  satfv1fvfmla1  35410  cgrcomim  35977  cgrcoml  35984  cgrcomr  35985  cgrdegen  35992  btwnintr  36007  btwnexch3  36008  btwnouttr2  36010  btwnouttr  36012  btwnexch  36013  btwndiff  36015  lineid  36071  idinside  36072  btwnconn1lem7  36081  btwnconn1lem8  36082  btwnconn1lem9  36083  btwnconn1lem12  36086  btwnconn1lem14  36088  btwnconn3  36091  midofsegid  36092  segcon2  36093  brsegle2  36097  btwnoutside  36113  outsideoftr  36117  outsideofeu  36119  linethru  36141  cnres2  37757  heibor  37815  lsmsat  39001  lkrlsp  39095  lkrlsp2  39096  lkrlsp3  39097  latm4  39226  omlspjN  39254  hlatj4  39367  4noncolr3  39447  4noncolr2  39448  4noncolr1  39449  athgt  39450  3dimlem3a  39454  3dimlem4a  39457  3dimlem4  39458  3dimlem4OLDN  39459  3dim3  39463  1cvratex  39467  hlatexch4  39475  3atlem4  39480  atcvrlln2  39513  atcvrlln  39514  lplnnlelln  39537  lvoli2  39575  lvolnlelln  39578  lvolnlelpln  39579  4atlem11b  39602  4atlem12b  39605  2lplnja  39613  2lplnj  39614  dalemyeo  39626  dath2  39731  lncvrat  39776  cdlemblem  39787  cdlemb  39788  elpaddri  39796  padd4N  39834  llnmod2i2  39857  llnexchb2  39863  dalawlem1  39865  dalawlem2  39866  pclfinN  39894  osumcllem6N  39955  pexmidlem3N  39966  lhp2lt  39995  lhp2at0  40026  lhp2atnle  40027  lhp2atne  40028  lhp2at0nle  40029  lhp2at0ne  40030  lhpelim  40031  lhpmod2i2  40032  lhpmod6i1  40033  lhple  40036  lhpat  40037  lhpat3  40040  ltrncoelN  40137  ltrncoat  40138  ltrncnv  40140  trlat  40163  trl0  40164  ltrnnidn  40168  trlnid  40173  cdlemd7  40198  cdleme0b  40206  cdleme0c  40207  cdleme0fN  40212  cdleme02N  40216  cdleme0ex1N  40217  cdleme0ex2N  40218  cdleme7aa  40236  cdleme7c  40239  cdleme7d  40240  cdleme7e  40241  cdleme7ga  40242  cdleme7  40243  cdleme8  40244  cdleme11a  40254  cdleme17c  40282  cdleme22gb  40288  cdlemeda  40292  cdleme20k  40313  cdleme21a  40319  cdleme21d  40324  cdleme22f2  40341  cdleme22g  40342  cdleme23a  40343  cdleme23b  40344  cdleme23c  40345  cdleme24  40346  cdleme28  40367  cdlemefrs32fva1  40395  cdlemefr32sn2aw  40398  cdlemefs32sn1aw  40408  cdleme41sn3a  40427  cdleme32fva  40431  cdleme32fva1  40432  cdleme35a  40442  cdleme35b  40444  cdleme35c  40445  cdleme35f  40448  cdleme39a  40459  cdleme42a  40465  cdleme42c  40466  cdleme42b  40472  cdleme42e  40473  cdleme42f  40474  cdleme42g  40475  cdleme42h  40476  cdleme43bN  40484  cdleme46f2g2  40487  cdleme17d2  40489  cdleme17d4  40491  cdleme48fv  40493  cdleme48fvg  40494  cdleme4gfv  40501  cdlemeg46c  40507  cdlemeg46nlpq  40511  cdlemeg46gfre  40526  cdleme48d  40529  cdlemeg49lebilem  40533  cdleme50trn2  40545  cdleme50ltrn  40551  cdleme  40554  cdlemf1  40555  cdlemf  40557  trlord  40563  ltrniotacnvval  40576  ltrniotavalbN  40578  cdlemg1cex  40582  cdlemg2dN  40584  cdlemg2ce  40586  cdlemg2fvlem  40588  cdlemg2idN  40590  cdlemg2kq  40596  cdlemg2l  40597  cdlemg2m  40598  cdlemg4b2  40604  cdlemg7fvN  40618  cdlemg8a  40621  cdlemg10bALTN  40630  cdlemg11aq  40632  cdlemg12d  40640  cdlemg13a  40645  cdlemg13  40646  cdlemg14f  40647  cdlemg14g  40648  cdlemg17a  40655  cdlemg17b  40656  cdlemg27a  40686  cdlemg31b0N  40688  cdlemg31a  40691  cdlemg31b  40692  cdlemg31c  40693  ltrnco  40713  trlcoabs  40715  trlcoabs2N  40716  trlcocnvat  40718  trlconid  40719  trlcolem  40720  trlcone  40722  cdlemg42  40723  cdlemg43  40724  cdlemg46  40729  cdlemg47  40730  tendoeq1  40758  tendoco2  40762  tendoplco2  40773  tendopltp  40774  cdlemh1  40809  cdlemh2  40810  cdlemi1  40812  cdlemi  40814  cdlemk1  40825  cdlemk2  40826  cdlemk3  40827  cdlemk4  40828  cdlemk8  40832  cdlemk9  40833  cdlemk9bN  40834  cdlemk31  40890  cdlemk32  40891  cdlemk28-3  40902  cdlemk19u  40964  cdlemk56w  40967  tendoex  40969  erngdvlem4  40985  erngdvlem4-rN  40993  dia11N  41042  dib11N  41154  cdlemn6  41196  cdlemn7  41197  cdlemn8  41198  cdlemn9  41199  dihordlem6  41207  dihordlem7  41208  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord2pre  41219  dihord2pre2  41220  dihlsscpre  41228  dihvalcq2  41241  dihopelvalcpre  41242  dihord4  41252  dihord6b  41254  dihmeetlem1N  41284  dihglblem3N  41289  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetcN  41296  dihmeetbclemN  41298  dihmeetlem4preN  41300  dihjatc1  41305  dihjatc2N  41306  dihjatc3  41307  dihmeetlem9N  41309  dihmeetlem13N  41313  dihmeetlem20N  41320  dih1dimatlem0  41322  mapdpglem24  41698  mapdpglem32  41699  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  mapdh9aOLDN  41784  hdmap14lem6  41867  nnadddir  42258  sn-addlid  42392  mzpsubst  42736  pellexlem5  42821  pellex  42823  pell14qrexpclnn0  42854  pellfundex  42874  qirropth  42896  monotuz  42930  congtr  42954  congmul  42956  congsub  42959  mzpcong  42961  fzmaxdif  42970  jm2.15nn0  42992  idomsubgmo  43182  iunrelexpmin1  43697  iunrelexpmin2  43701  trclimalb2  43715  mnringmulrcld  44217  fourierdlem42  46147  fourierdlem48  46152  fourierdlem80  46184  smfaddlem1  46761  prmdvdsfmtnof1lem1  47585  uhgrimisgrgric  47931  uspgropssxp  48132  lidldomn1  48219  rngccatidALTV  48260  coe1sclmulval  48374  lincdifsn  48413  seposep  48914  iscnrm3rlem8  48935  iscnrm3llem2  48938