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  7125  f1oiso2  7293  fpr3g  8225  omeulem2  8508  uniinqs  8731  unxpdomlem3  9157  gruina  10731  dedekind  11297  addlid  11317  subaddmulsub  11601  dmdcan  11852  xaddass  13169  xaddass2  13170  xlt2add  13180  xmulasslem3  13206  xadddi2  13217  xadddi2r  13218  expaddzlem  14030  expaddz  14031  expmulz  14033  expdiv  14038  expmordi  14092  modexp  14163  pfxeq  14620  ccatopth2  14641  swrdco  14762  o1add  15539  o1mul  15540  o1sub  15541  fsumsplitsnun  15680  ntrivcvgmul  15827  prmexpb  16648  pcpremul  16773  pcdiv  16782  pcqmul  16783  pcqdiv  16787  4sqlem12  16886  f1ocpbllem  17446  ercpbl  17471  erlecpbl  17472  latjlej12  18379  latmlem12  18395  latj4  18413  latj4rot  18414  gsumsgrpccat  18732  gsmsymgreqlem2  19328  symgsssg  19364  symgfisg  19365  mndodcong  19439  cmn4  19698  ablsub4  19707  abladdsub4  19708  lsm4  19757  abvdom  20733  abvres  20734  abvtrivd  20735  orngmul  20768  lspsnvs  21039  lspsneu  21048  lspfixed  21053  lspexch  21054  lsmcv  21066  lspsolvlem  21067  ring2idlqus1  21244  coe1sclmulfv  22185  matvscacell  22339  m1detdiag  22500  cramerimplem3  22588  cnprest  23192  hausnei2  23256  isreg2  23280  cmpcld  23305  llyrest  23388  nllyrest  23389  elptr  23476  basqtop  23614  hausflimlem  23882  tmdgsum  23998  utop2nei  24154  trcfilu  24197  ssblps  24326  ssbl  24327  prdsxmslem2  24433  tgqioo  24704  metnrm  24767  bndth  24873  ncvspi  25072  ncvs1  25073  cph2ass  25129  lmmbr2  25175  iscau3  25194  bcthlem5  25244  ovolunlem2  25415  dvres2  25829  dvfsumlem2  25949  dvfsumlem2OLD  25950  plyadd  26138  plymul  26139  coeeu  26146  coemullem  26171  aalioulem4  26259  mulcxp  26610  cxplea  26621  cxple2  26622  cxplt2  26623  cxpcn3lem  26673  angcan  26728  ang180lem5  26739  divsqrtsumlem  26906  logexprlim  27152  dchrvmasumlema  27427  dchrisum0lema  27441  logdivsum  27460  log2sumbnd  27471  abvcxp  27542  padicabv  27557  nolesgn2ores  27600  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem2  27637  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd1lem6  27641  noinffv  27649  noinfres  27650  noinfbnd1lem1  27651  noinfbnd1lem2  27652  noinfbnd1lem4  27654  noinfbnd1lem6  27656  nosupinfsep  27660  scutbdaylt  27747  expsgt0  28347  tghilberti2  28601  brbtwn2  28868  axcontlem4  28930  axcontlem8  28934  clwlkl1loop  29746  clwwlknonex2lem2  30070  clwlknon2num  30330  numclwlk1lem2  30332  chscllem4  31602  measxun2  34176  measun  34177  mbfmco2  34232  probun  34386  satfv1fvfmla1  35395  cgrcomim  35962  cgrcoml  35969  cgrcomr  35970  cgrdegen  35977  btwnintr  35992  btwnexch3  35993  btwnouttr2  35995  btwnouttr  35997  btwnexch  35998  btwndiff  36000  lineid  36056  idinside  36057  btwnconn1lem7  36066  btwnconn1lem8  36067  btwnconn1lem9  36068  btwnconn1lem12  36071  btwnconn1lem14  36073  btwnconn3  36076  midofsegid  36077  segcon2  36078  brsegle2  36082  btwnoutside  36098  outsideoftr  36102  outsideofeu  36104  linethru  36126  cnres2  37742  heibor  37800  lsmsat  38986  lkrlsp  39080  lkrlsp2  39081  lkrlsp3  39082  latm4  39211  omlspjN  39239  hlatj4  39352  4noncolr3  39432  4noncolr2  39433  4noncolr1  39434  athgt  39435  3dimlem3a  39439  3dimlem4a  39442  3dimlem4  39443  3dimlem4OLDN  39444  3dim3  39448  1cvratex  39452  hlatexch4  39460  3atlem4  39465  atcvrlln2  39498  atcvrlln  39499  lplnnlelln  39522  lvoli2  39560  lvolnlelln  39563  lvolnlelpln  39564  4atlem11b  39587  4atlem12b  39590  2lplnja  39598  2lplnj  39599  dalemyeo  39611  dath2  39716  lncvrat  39761  cdlemblem  39772  cdlemb  39773  elpaddri  39781  padd4N  39819  llnmod2i2  39842  llnexchb2  39848  dalawlem1  39850  dalawlem2  39851  pclfinN  39879  osumcllem6N  39940  pexmidlem3N  39951  lhp2lt  39980  lhp2at0  40011  lhp2atnle  40012  lhp2atne  40013  lhp2at0nle  40014  lhp2at0ne  40015  lhpelim  40016  lhpmod2i2  40017  lhpmod6i1  40018  lhple  40021  lhpat  40022  lhpat3  40025  ltrncoelN  40122  ltrncoat  40123  ltrncnv  40125  trlat  40148  trl0  40149  ltrnnidn  40153  trlnid  40158  cdlemd7  40183  cdleme0b  40191  cdleme0c  40192  cdleme0fN  40197  cdleme02N  40201  cdleme0ex1N  40202  cdleme0ex2N  40203  cdleme7aa  40221  cdleme7c  40224  cdleme7d  40225  cdleme7e  40226  cdleme7ga  40227  cdleme7  40228  cdleme8  40229  cdleme11a  40239  cdleme17c  40267  cdleme22gb  40273  cdlemeda  40277  cdleme20k  40298  cdleme21a  40304  cdleme21d  40309  cdleme22f2  40326  cdleme22g  40327  cdleme23a  40328  cdleme23b  40329  cdleme23c  40330  cdleme24  40331  cdleme28  40352  cdlemefrs32fva1  40380  cdlemefr32sn2aw  40383  cdlemefs32sn1aw  40393  cdleme41sn3a  40412  cdleme32fva  40416  cdleme32fva1  40417  cdleme35a  40427  cdleme35b  40429  cdleme35c  40430  cdleme35f  40433  cdleme39a  40444  cdleme42a  40450  cdleme42c  40451  cdleme42b  40457  cdleme42e  40458  cdleme42f  40459  cdleme42g  40460  cdleme42h  40461  cdleme43bN  40469  cdleme46f2g2  40472  cdleme17d2  40474  cdleme17d4  40476  cdleme48fv  40478  cdleme48fvg  40479  cdleme4gfv  40486  cdlemeg46c  40492  cdlemeg46nlpq  40496  cdlemeg46gfre  40511  cdleme48d  40514  cdlemeg49lebilem  40518  cdleme50trn2  40530  cdleme50ltrn  40536  cdleme  40539  cdlemf1  40540  cdlemf  40542  trlord  40548  ltrniotacnvval  40561  ltrniotavalbN  40563  cdlemg1cex  40567  cdlemg2dN  40569  cdlemg2ce  40571  cdlemg2fvlem  40573  cdlemg2idN  40575  cdlemg2kq  40581  cdlemg2l  40582  cdlemg2m  40583  cdlemg4b2  40589  cdlemg7fvN  40603  cdlemg8a  40606  cdlemg10bALTN  40615  cdlemg11aq  40617  cdlemg12d  40625  cdlemg13a  40630  cdlemg13  40631  cdlemg14f  40632  cdlemg14g  40633  cdlemg17a  40640  cdlemg17b  40641  cdlemg27a  40671  cdlemg31b0N  40673  cdlemg31a  40676  cdlemg31b  40677  cdlemg31c  40678  ltrnco  40698  trlcoabs  40700  trlcoabs2N  40701  trlcocnvat  40703  trlconid  40704  trlcolem  40705  trlcone  40707  cdlemg42  40708  cdlemg43  40709  cdlemg46  40714  cdlemg47  40715  tendoeq1  40743  tendoco2  40747  tendoplco2  40758  tendopltp  40759  cdlemh1  40794  cdlemh2  40795  cdlemi1  40797  cdlemi  40799  cdlemk1  40810  cdlemk2  40811  cdlemk3  40812  cdlemk4  40813  cdlemk8  40817  cdlemk9  40818  cdlemk9bN  40819  cdlemk31  40875  cdlemk32  40876  cdlemk28-3  40887  cdlemk19u  40949  cdlemk56w  40952  tendoex  40954  erngdvlem4  40970  erngdvlem4-rN  40978  dia11N  41027  dib11N  41139  cdlemn6  41181  cdlemn7  41182  cdlemn8  41183  cdlemn9  41184  dihordlem6  41192  dihordlem7  41193  dihord1  41197  dihord2a  41198  dihord2b  41199  dihord2pre  41204  dihord2pre2  41205  dihlsscpre  41213  dihvalcq2  41226  dihopelvalcpre  41227  dihord4  41237  dihord6b  41239  dihmeetlem1N  41269  dihglblem3N  41274  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetcN  41281  dihmeetbclemN  41283  dihmeetlem4preN  41285  dihjatc1  41290  dihjatc2N  41291  dihjatc3  41292  dihmeetlem9N  41294  dihmeetlem13N  41298  dihmeetlem20N  41305  dih1dimatlem0  41307  mapdpglem24  41683  mapdpglem32  41684  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  mapdh9aOLDN  41769  hdmap14lem6  41852  nnadddir  42243  sn-addlid  42377  mzpsubst  42721  pellexlem5  42806  pellex  42808  pell14qrexpclnn0  42839  pellfundex  42859  qirropth  42881  monotuz  42914  congtr  42938  congmul  42940  congsub  42943  mzpcong  42945  fzmaxdif  42954  jm2.15nn0  42976  idomsubgmo  43166  iunrelexpmin1  43681  iunrelexpmin2  43685  trclimalb2  43699  mnringmulrcld  44201  fourierdlem42  46131  fourierdlem48  46136  fourierdlem80  46168  smfaddlem1  46745  prmdvdsfmtnof1lem1  47569  uhgrimisgrgric  47916  uspgropssxp  48129  lidldomn1  48216  rngccatidALTV  48257  coe1sclmulval  48371  lincdifsn  48410  seposep  48911  iscnrm3rlem8  48932  iscnrm3llem2  48935