Theorem simp2l 1218

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 488	. 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:  simp12l  1305  simp22l  1311  simp32l  1317  fsnunf  7187  f1resrcmplf1d  7276  f1oiso2  7357  fpr3g  8288  omeulem2  8574  uniinqs  8801  unxpdomlem3  9232  gruina  10831  dedekind  11401  addlid  11421  subaddmulsub  11705  dmdcan  11953  nnadddir  12320  xaddass  13305  xaddass2  13306  xlt2add  13316  xmulasslem3  13342  xadddi2  13353  xadddi2r  13354  expaddzlem  14173  expaddz  14174  expmulz  14176  expdiv  14181  expmordi  14235  modexp  14306  pfxeq  14769  ccatopth2  14790  swrdco  14912  o1add  15705  o1mul  15706  o1sub  15707  fsumsplitsnun  15845  ntrivcvgmul  15995  prmexpb  16816  pcpremul  16941  pcdiv  16950  pcqmul  16951  pcqdiv  16955  4sqlem12  17054  f1ocpbllem  17616  ercpbl  17641  erlecpbl  17642  latjlej12  18549  latmlem12  18565  latj4  18583  latj4rot  18584  gsumsgrpccat  18955  gsmsymgreqlem2  19564  symgsssg  19600  symgfisg  19601  mndodcong  19675  cmn4  19934  ablsub4  19943  abladdsub4  19944  lsm4  19993  abvdom  21002  abvres  21003  abvtrivd  21004  orngmul  21037  lspsnvs  21307  lspsneu  21316  lspfixed  21321  lspexch  21322  lsmcv  21334  lspsolvlem  21335  ring2idlqus1  21528  coe1sclmulfv  22515  matvscacell  22664  m1detdiag  22825  cramerimplem3  22916  cnprest  23520  hausnei2  23584  isreg2  23608  cmpcld  23633  llyrest  23717  nllyrest  23718  elptr  23805  basqtop  23943  hausflimlem  24211  tmdgsum  24327  utop2nei  24482  trcfilu  24525  ssblps  24654  ssbl  24655  prdsxmslem2  24761  tgqioo  25032  metnrm  25095  bndth  25192  ncvspi  25390  ncvs1  25391  cph2ass  25447  lmmbr2  25493  iscau3  25512  bcthlem5  25562  ovolunlem2  25732  dvres2  26146  dvfsumlem2  26261  plyadd  26450  plymul  26451  coeeu  26458  coemullem  26483  aalioulem4  26578  mulcxp  26930  cxplea  26941  cxple2  26942  cxplt2  26943  cxpcn3lem  26992  angcan  27047  ang180lem5  27058  divsqrtsumlem  27224  logexprlim  27469  dchrvmasumlema  27744  dchrisum0lema  27758  logdivsum  27777  log2sumbnd  27788  abvcxp  27859  padicabv  27874  nolesgn2ores  27916  nosupres  27951  nosupbnd1lem1  27952  nosupbnd1lem2  27953  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd1lem6  27957  noinffv  27965  noinfres  27966  noinfbnd1lem1  27967  noinfbnd1lem2  27968  noinfbnd1lem4  27970  noinfbnd1lem6  27972  nosupinfsep  27976  cutbdaylt  28071  expsgt0  28710  bdayfinbndlem1  28740  tghilberti2  28993  brbtwn2  29370  axcontlem4  29432  axcontlem8  29436  clwlkl1loop  30257  clwwlknonex2lem2  30586  umgr2cycllem  30633  clwlknon2num  30856  numclwlk1lem2  30858  chscllem4  32129  measxun2  34729  measun  34730  mbfmco2  34784  probun  34938  satfv1fvfmla1  36010  cgrcomim  36577  cgrcoml  36584  cgrcomr  36585  cgrdegen  36592  btwnintr  36607  btwnexch3  36608  btwnouttr2  36610  btwnouttr  36612  btwnexch  36613  btwndiff  36615  lineid  36671  idinside  36672  btwnconn1lem7  36681  btwnconn1lem8  36682  btwnconn1lem9  36683  btwnconn1lem12  36686  btwnconn1lem14  36688  btwnconn3  36691  midofsegid  36692  segcon2  36693  brsegle2  36697  btwnoutside  36713  outsideoftr  36717  outsideofeu  36719  linethru  36741  cnres2  38521  heibor  38579  lsmsat  39889  lkrlsp  39983  lkrlsp2  39984  lkrlsp3  39985  latm4  40114  omlspjN  40142  hlatj4  40255  4noncolr3  40334  4noncolr2  40335  4noncolr1  40336  athgt  40337  3dimlem3a  40341  3dimlem4a  40344  3dimlem4  40345  3dimlem4OLDN  40346  3dim3  40350  1cvratex  40354  hlatexch4  40362  3atlem4  40367  atcvrlln2  40400  atcvrlln  40401  lplnnlelln  40424  lvoli2  40462  lvolnlelln  40465  lvolnlelpln  40466  4atlem11b  40489  4atlem12b  40492  2lplnja  40500  2lplnj  40501  dalemyeo  40513  dath2  40618  lncvrat  40663  cdlemblem  40674  cdlemb  40675  elpaddri  40683  padd4N  40721  llnmod2i2  40744  llnexchb2  40750  dalawlem1  40752  dalawlem2  40753  pclfinN  40781  osumcllem6N  40842  pexmidlem3N  40853  lhp2lt  40882  lhp2at0  40913  lhp2atnle  40914  lhp2atne  40915  lhp2at0nle  40916  lhp2at0ne  40917  lhpelim  40918  lhpmod2i2  40919  lhpmod6i1  40920  lhple  40923  lhpat  40924  lhpat3  40927  ltrncoelN  41024  ltrncoat  41025  ltrncnv  41027  trlat  41050  trl0  41051  ltrnnidn  41055  trlnid  41060  cdlemd7  41085  cdleme0b  41093  cdleme0c  41094  cdleme0fN  41099  cdleme02N  41103  cdleme0ex1N  41104  cdleme0ex2N  41105  cdleme7aa  41123  cdleme7c  41126  cdleme7d  41127  cdleme7e  41128  cdleme7ga  41129  cdleme7  41130  cdleme8  41131  cdleme11a  41141  cdleme17c  41169  cdleme22gb  41175  cdlemeda  41179  cdleme20k  41200  cdleme21a  41206  cdleme21d  41211  cdleme22f2  41228  cdleme22g  41229  cdleme23a  41230  cdleme23b  41231  cdleme23c  41232  cdleme24  41233  cdleme28  41254  cdlemefrs32fva1  41282  cdlemefr32sn2aw  41285  cdlemefs32sn1aw  41295  cdleme41sn3a  41314  cdleme32fva  41318  cdleme32fva1  41319  cdleme35a  41329  cdleme35b  41331  cdleme35c  41332  cdleme35f  41335  cdleme39a  41346  cdleme42a  41352  cdleme42c  41353  cdleme42b  41359  cdleme42e  41360  cdleme42f  41361  cdleme42g  41362  cdleme42h  41363  cdleme43bN  41371  cdleme46f2g2  41374  cdleme17d2  41376  cdleme17d4  41378  cdleme48fv  41380  cdleme48fvg  41381  cdleme4gfv  41388  cdlemeg46c  41394  cdlemeg46nlpq  41398  cdlemeg46gfre  41413  cdleme48d  41416  cdlemeg49lebilem  41420  cdleme50trn2  41432  cdleme50ltrn  41438  cdleme  41441  cdlemf1  41442  cdlemf  41444  trlord  41450  ltrniotacnvval  41463  ltrniotavalbN  41465  cdlemg1cex  41469  cdlemg2dN  41471  cdlemg2ce  41473  cdlemg2fvlem  41475  cdlemg2idN  41477  cdlemg2kq  41483  cdlemg2l  41484  cdlemg2m  41485  cdlemg4b2  41491  cdlemg7fvN  41505  cdlemg8a  41508  cdlemg10bALTN  41517  cdlemg11aq  41519  cdlemg12d  41527  cdlemg13a  41532  cdlemg13  41533  cdlemg14f  41534  cdlemg14g  41535  cdlemg17a  41542  cdlemg17b  41543  cdlemg27a  41573  cdlemg31b0N  41575  cdlemg31a  41578  cdlemg31b  41579  cdlemg31c  41580  ltrnco  41600  trlcoabs  41602  trlcoabs2N  41603  trlcocnvat  41605  trlconid  41606  trlcolem  41607  trlcone  41609  cdlemg42  41610  cdlemg43  41611  cdlemg46  41616  cdlemg47  41617  tendoeq1  41645  tendoco2  41649  tendoplco2  41660  tendopltp  41661  cdlemh1  41696  cdlemh2  41697  cdlemi1  41699  cdlemi  41701  cdlemk1  41712  cdlemk2  41713  cdlemk3  41714  cdlemk4  41715  cdlemk8  41719  cdlemk9  41720  cdlemk9bN  41721  cdlemk31  41777  cdlemk32  41778  cdlemk28-3  41789  cdlemk19u  41851  cdlemk56w  41854  tendoex  41856  erngdvlem4  41872  erngdvlem4-rN  41880  dia11N  41929  dib11N  42041  cdlemn6  42083  cdlemn7  42084  cdlemn8  42085  cdlemn9  42086  dihordlem6  42094  dihordlem7  42095  dihord1  42099  dihord2a  42100  dihord2b  42101  dihord2pre  42106  dihord2pre2  42107  dihlsscpre  42115  dihvalcq2  42128  dihopelvalcpre  42129  dihord4  42139  dihord6b  42141  dihmeetlem1N  42171  dihglblem3N  42176  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetcN  42183  dihmeetbclemN  42185  dihmeetlem4preN  42187  dihjatc1  42192  dihjatc2N  42193  dihjatc3  42194  dihmeetlem9N  42196  dihmeetlem13N  42200  dihmeetlem20N  42207  dih1dimatlem0  42209  mapdpglem24  42585  mapdpglem32  42586  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  mapdh9aOLDN  42671  hdmap14lem6  42754  sn-addlid  43287  mzpsubst  43601  pellexlem5  43682  pellex  43684  pell14qrexpclnn0  43715  pellfundex  43735  qirropth  43757  monotuz  43790  congtr  43814  congmul  43816  congsub  43819  mzpcong  43821  fzmaxdif  43830  jm2.15nn0  43852  idomsubgmo  44042  iunrelexpmin1  44556  iunrelexpmin2  44560  trclimalb2  44574  mnringmulrcld  45074  fourierdlem42  46985  fourierdlem48  46990  fourierdlem80  47022  smfaddlem1  47599  prmdvdsfmtnof1lem1  48495  uhgrimisgrgric  48855  uspgropssxp  49068  lidldomn1  49154  rngccatidALTV  49195  coe1sclmulval  49323  lincdifsn  49362  seposep  49860  iscnrm3rlem8  49881  iscnrm3llem2  49884