Theorem simp2l 1216

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simp12l  1303  simp22l  1309  simp32l  1315  fsnunf  7173  f1oiso2  7340  fpr3g  8270  omeulem2  8556  uniinqs  8783  unxpdomlem3  9206  gruina  10791  dedekind  11361  addlid  11381  subaddmulsub  11665  dmdcan  11916  nnadddir  12283  xaddass  13266  xaddass2  13267  xlt2add  13277  xmulasslem3  13303  xadddi2  13314  xadddi2r  13315  expaddzlem  14132  expaddz  14133  expmulz  14135  expdiv  14140  expmordi  14194  modexp  14265  pfxeq  14723  ccatopth2  14744  swrdco  14864  o1add  15655  o1mul  15656  o1sub  15657  fsumsplitsnun  15796  ntrivcvgmul  15946  prmexpb  16768  pcpremul  16893  pcdiv  16902  pcqmul  16903  pcqdiv  16907  4sqlem12  17006  f1ocpbllem  17568  ercpbl  17593  erlecpbl  17594  latjlej12  18501  latmlem12  18517  latj4  18535  latj4rot  18536  gsumsgrpccat  18889  gsmsymgreqlem2  19492  symgsssg  19528  symgfisg  19529  mndodcong  19603  cmn4  19862  ablsub4  19871  abladdsub4  19872  lsm4  19921  abvdom  20902  abvres  20903  abvtrivd  20904  orngmul  20937  lspsnvs  21207  lspsneu  21216  lspfixed  21221  lspexch  21222  lsmcv  21234  lspsolvlem  21235  ring2idlqus1  21421  coe1sclmulfv  22404  matvscacell  22554  m1detdiag  22715  cramerimplem3  22803  cnprest  23407  hausnei2  23471  isreg2  23495  cmpcld  23520  llyrest  23603  nllyrest  23604  elptr  23691  basqtop  23829  hausflimlem  24097  tmdgsum  24213  utop2nei  24368  trcfilu  24411  ssblps  24540  ssbl  24541  prdsxmslem2  24647  tgqioo  24918  metnrm  24981  bndth  25078  ncvspi  25276  ncvs1  25277  cph2ass  25333  lmmbr2  25379  iscau3  25398  bcthlem5  25448  ovolunlem2  25618  dvres2  26032  dvfsumlem2  26147  plyadd  26335  plymul  26336  coeeu  26343  coemullem  26368  aalioulem4  26457  mulcxp  26808  cxplea  26819  cxple2  26820  cxplt2  26821  cxpcn3lem  26870  angcan  26925  ang180lem5  26936  divsqrtsumlem  27102  logexprlim  27347  dchrvmasumlema  27622  dchrisum0lema  27636  logdivsum  27655  log2sumbnd  27666  abvcxp  27737  padicabv  27752  nolesgn2ores  27794  nosupres  27829  nosupbnd1lem1  27830  nosupbnd1lem2  27831  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd1lem6  27835  noinffv  27843  noinfres  27844  noinfbnd1lem1  27845  noinfbnd1lem2  27846  noinfbnd1lem4  27848  noinfbnd1lem6  27850  nosupinfsep  27854  cutbdaylt  27949  expsgt0  28588  bdayfinbndlem1  28618  tghilberti2  28865  brbtwn2  29164  axcontlem4  29226  axcontlem8  29230  clwlkl1loop  30041  clwwlknonex2lem2  30368  clwlknon2num  30628  numclwlk1lem2  30630  chscllem4  31901  measxun2  34517  measun  34518  mbfmco2  34572  probun  34726  satfv1fvfmla1  35786  cgrcomim  36352  cgrcoml  36359  cgrcomr  36360  cgrdegen  36367  btwnintr  36382  btwnexch3  36383  btwnouttr2  36385  btwnouttr  36387  btwnexch  36388  btwndiff  36390  lineid  36446  idinside  36447  btwnconn1lem7  36456  btwnconn1lem8  36457  btwnconn1lem9  36458  btwnconn1lem12  36461  btwnconn1lem14  36463  btwnconn3  36466  midofsegid  36467  segcon2  36468  brsegle2  36472  btwnoutside  36488  outsideoftr  36492  outsideofeu  36494  linethru  36516  cnres2  38274  heibor  38332  lsmsat  39644  lkrlsp  39738  lkrlsp2  39739  lkrlsp3  39740  latm4  39869  omlspjN  39897  hlatj4  40010  4noncolr3  40089  4noncolr2  40090  4noncolr1  40091  athgt  40092  3dimlem3a  40096  3dimlem4a  40099  3dimlem4  40100  3dimlem4OLDN  40101  3dim3  40105  1cvratex  40109  hlatexch4  40117  3atlem4  40122  atcvrlln2  40155  atcvrlln  40156  lplnnlelln  40179  lvoli2  40217  lvolnlelln  40220  lvolnlelpln  40221  4atlem11b  40244  4atlem12b  40247  2lplnja  40255  2lplnj  40256  dalemyeo  40268  dath2  40373  lncvrat  40418  cdlemblem  40429  cdlemb  40430  elpaddri  40438  padd4N  40476  llnmod2i2  40499  llnexchb2  40505  dalawlem1  40507  dalawlem2  40508  pclfinN  40536  osumcllem6N  40597  pexmidlem3N  40608  lhp2lt  40637  lhp2at0  40668  lhp2atnle  40669  lhp2atne  40670  lhp2at0nle  40671  lhp2at0ne  40672  lhpelim  40673  lhpmod2i2  40674  lhpmod6i1  40675  lhple  40678  lhpat  40679  lhpat3  40682  ltrncoelN  40779  ltrncoat  40780  ltrncnv  40782  trlat  40805  trl0  40806  ltrnnidn  40810  trlnid  40815  cdlemd7  40840  cdleme0b  40848  cdleme0c  40849  cdleme0fN  40854  cdleme02N  40858  cdleme0ex1N  40859  cdleme0ex2N  40860  cdleme7aa  40878  cdleme7c  40881  cdleme7d  40882  cdleme7e  40883  cdleme7ga  40884  cdleme7  40885  cdleme8  40886  cdleme11a  40896  cdleme17c  40924  cdleme22gb  40930  cdlemeda  40934  cdleme20k  40955  cdleme21a  40961  cdleme21d  40966  cdleme22f2  40983  cdleme22g  40984  cdleme23a  40985  cdleme23b  40986  cdleme23c  40987  cdleme24  40988  cdleme28  41009  cdlemefrs32fva1  41037  cdlemefr32sn2aw  41040  cdlemefs32sn1aw  41050  cdleme41sn3a  41069  cdleme32fva  41073  cdleme32fva1  41074  cdleme35a  41084  cdleme35b  41086  cdleme35c  41087  cdleme35f  41090  cdleme39a  41101  cdleme42a  41107  cdleme42c  41108  cdleme42b  41114  cdleme42e  41115  cdleme42f  41116  cdleme42g  41117  cdleme42h  41118  cdleme43bN  41126  cdleme46f2g2  41129  cdleme17d2  41131  cdleme17d4  41133  cdleme48fv  41135  cdleme48fvg  41136  cdleme4gfv  41143  cdlemeg46c  41149  cdlemeg46nlpq  41153  cdlemeg46gfre  41168  cdleme48d  41171  cdlemeg49lebilem  41175  cdleme50trn2  41187  cdleme50ltrn  41193  cdleme  41196  cdlemf1  41197  cdlemf  41199  trlord  41205  ltrniotacnvval  41218  ltrniotavalbN  41220  cdlemg1cex  41224  cdlemg2dN  41226  cdlemg2ce  41228  cdlemg2fvlem  41230  cdlemg2idN  41232  cdlemg2kq  41238  cdlemg2l  41239  cdlemg2m  41240  cdlemg4b2  41246  cdlemg7fvN  41260  cdlemg8a  41263  cdlemg10bALTN  41272  cdlemg11aq  41274  cdlemg12d  41282  cdlemg13a  41287  cdlemg13  41288  cdlemg14f  41289  cdlemg14g  41290  cdlemg17a  41297  cdlemg17b  41298  cdlemg27a  41328  cdlemg31b0N  41330  cdlemg31a  41333  cdlemg31b  41334  cdlemg31c  41335  ltrnco  41355  trlcoabs  41357  trlcoabs2N  41358  trlcocnvat  41360  trlconid  41361  trlcolem  41362  trlcone  41364  cdlemg42  41365  cdlemg43  41366  cdlemg46  41371  cdlemg47  41372  tendoeq1  41400  tendoco2  41404  tendoplco2  41415  tendopltp  41416  cdlemh1  41451  cdlemh2  41452  cdlemi1  41454  cdlemi  41456  cdlemk1  41467  cdlemk2  41468  cdlemk3  41469  cdlemk4  41470  cdlemk8  41474  cdlemk9  41475  cdlemk9bN  41476  cdlemk31  41532  cdlemk32  41533  cdlemk28-3  41544  cdlemk19u  41606  cdlemk56w  41609  tendoex  41611  erngdvlem4  41627  erngdvlem4-rN  41635  dia11N  41684  dib11N  41796  cdlemn6  41838  cdlemn7  41839  cdlemn8  41840  cdlemn9  41841  dihordlem6  41849  dihordlem7  41850  dihord1  41854  dihord2a  41855  dihord2b  41856  dihord2pre  41861  dihord2pre2  41862  dihlsscpre  41870  dihvalcq2  41883  dihopelvalcpre  41884  dihord4  41894  dihord6b  41896  dihmeetlem1N  41926  dihglblem3N  41931  dihmeetlem2N  41935  dihglbcpreN  41936  dihmeetcN  41938  dihmeetbclemN  41940  dihmeetlem4preN  41942  dihjatc1  41947  dihjatc2N  41948  dihjatc3  41949  dihmeetlem9N  41951  dihmeetlem13N  41955  dihmeetlem20N  41962  dih1dimatlem0  41964  mapdpglem24  42340  mapdpglem32  42341  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  mapdh9aOLDN  42426  hdmap14lem6  42509  sn-addlid  43025  mzpsubst  43341  pellexlem5  43422  pellex  43424  pell14qrexpclnn0  43455  pellfundex  43475  qirropth  43497  monotuz  43530  congtr  43554  congmul  43556  congsub  43559  mzpcong  43561  fzmaxdif  43570  jm2.15nn0  43592  idomsubgmo  43782  iunrelexpmin1  44296  iunrelexpmin2  44300  trclimalb2  44314  mnringmulrcld  44816  fourierdlem42  46721  fourierdlem48  46726  fourierdlem80  46758  smfaddlem1  47335  prmdvdsfmtnof1lem1  48191  uhgrimisgrgric  48551  uspgropssxp  48764  lidldomn1  48851  rngccatidALTV  48892  coe1sclmulval  49016  lincdifsn  49055  seposep  49555  iscnrm3rlem8  49576  iscnrm3llem2  49579