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  7190  f1resrcmplf1d  7279  f1oiso2  7360  fpr3g  8306  omeulem2  8594  uniinqs  8821  unxpdomlem3  9252  gruina  10906  dedekind  11476  addlid  11496  subaddmulsub  11782  dmdcan  12030  nnadddir  12397  xaddass  13382  xaddass2  13383  xlt2add  13393  xmulasslem3  13419  xadddi2  13430  xadddi2r  13431  expaddzlem  14251  expaddz  14252  expmulz  14254  expdiv  14259  expmordi  14313  modexp  14385  pfxeq  14849  ccatopth2  14870  swrdco  14992  o1add  15786  o1mul  15787  o1sub  15788  fsumsplitsnun  15926  ntrivcvgmul  16076  prmexpb  16900  pcpremul  17026  pcdiv  17035  pcqmul  17036  pcqdiv  17040  4sqlem12  17139  f1ocpbllem  17701  ercpbl  17726  erlecpbl  17727  latjlej12  18634  latmlem12  18650  latj4  18668  latj4rot  18669  gsumsgrpccat  19041  gsmsymgreqlem2  19650  symgsssg  19686  symgfisg  19687  mndodcong  19761  cmn4  20020  ablsub4  20029  abladdsub4  20030  lsm4  20079  abvdom  21092  abvres  21093  abvtrivd  21094  orngmul  21127  lspsnvs  21397  lspsneu  21406  lspfixed  21411  lspexch  21412  lsmcv  21424  lspsolvlem  21425  ring2idlqus1  21620  coe1sclmulfv  22607  matvscacell  22756  m1detdiag  22917  cramerimplem3  23008  cnprest  23612  hausnei2  23676  isreg2  23700  cmpcld  23725  llyrest  23809  nllyrest  23810  elptr  23897  basqtop  24035  hausflimlem  24303  tmdgsum  24419  utop2nei  24574  trcfilu  24617  ssblps  24746  ssbl  24747  prdsxmslem2  24853  tgqioo  25124  metnrm  25187  bndth  25284  ncvspi  25482  ncvs1  25483  cph2ass  25539  lmmbr2  25585  iscau3  25604  bcthlem5  25654  ovolunlem2  25824  dvres2  26237  dvfsumlem2  26352  plyadd  26541  plymul  26542  coeeu  26549  coemullem  26574  aalioulem4  26667  mulcxp  27018  cxplea  27029  cxple2  27030  cxplt2  27031  cxpcn3lem  27080  angcan  27135  ang180lem5  27146  divsqrtsumlem  27312  logexprlim  27557  dchrvmasumlema  27832  dchrisum0lema  27846  logdivsum  27865  log2sumbnd  27876  abvcxp  27947  padicabv  27962  nolesgn2ores  28034  nosupres  28069  nosupbnd1lem1  28070  nosupbnd1lem2  28071  nosupbnd1lem4  28073  nosupbnd1lem5  28074  nosupbnd1lem6  28075  noinffv  28083  noinfres  28084  noinfbnd1lem1  28085  noinfbnd1lem2  28086  noinfbnd1lem4  28088  noinfbnd1lem6  28090  nosupinfsep  28094  cutbdaylt  28189  expsgt0  28828  bdayfinbndlem1  28858  tghilberti2  29111  brbtwn2  29488  axcontlem4  29550  axcontlem8  29554  clwlkl1loop  30375  clwwlknonex2lem2  30704  umgr2cycllem  30751  clwlknon2num  30974  numclwlk1lem2  30976  chscllem4  32247  measxun2  34889  measun  34890  mbfmco2  34943  probun  35097  satfv1fvfmla1  36274  cgrcomim  36846  cgrcoml  36853  cgrcomr  36854  cgrdegen  36861  btwnintr  36876  btwnexch3  36877  btwnouttr2  36879  btwnouttr  36881  btwnexch  36882  btwndiff  36884  lineid  36940  idinside  36941  btwnconn1lem7  36950  btwnconn1lem8  36951  btwnconn1lem9  36952  btwnconn1lem12  36955  btwnconn1lem14  36957  btwnconn3  36960  midofsegid  36961  segcon2  36962  brsegle2  36966  btwnoutside  36982  outsideoftr  36986  outsideofeu  36988  linethru  37010  cnres2  38790  heibor  38848  lsmsat  40158  lkrlsp  40252  lkrlsp2  40253  lkrlsp3  40254  latm4  40383  omlspjN  40411  hlatj4  40524  4noncolr3  40603  4noncolr2  40604  4noncolr1  40605  athgt  40606  3dimlem3a  40610  3dimlem4a  40613  3dimlem4  40614  3dimlem4OLDN  40615  3dim3  40619  1cvratex  40623  hlatexch4  40631  3atlem4  40636  atcvrlln2  40669  atcvrlln  40670  lplnnlelln  40693  lvoli2  40731  lvolnlelln  40734  lvolnlelpln  40735  4atlem11b  40758  4atlem12b  40761  2lplnja  40769  2lplnj  40770  dalemyeo  40782  dath2  40887  lncvrat  40932  cdlemblem  40943  cdlemb  40944  elpaddri  40952  padd4N  40990  llnmod2i2  41013  llnexchb2  41019  dalawlem1  41021  dalawlem2  41022  pclfinN  41050  osumcllem6N  41111  pexmidlem3N  41122  lhp2lt  41151  lhp2at0  41182  lhp2atnle  41183  lhp2atne  41184  lhp2at0nle  41185  lhp2at0ne  41186  lhpelim  41187  lhpmod2i2  41188  lhpmod6i1  41189  lhple  41192  lhpat  41193  lhpat3  41196  ltrncoelN  41293  ltrncoat  41294  ltrncnv  41296  trlat  41319  trl0  41320  ltrnnidn  41324  trlnid  41329  cdlemd7  41354  cdleme0b  41362  cdleme0c  41363  cdleme0fN  41368  cdleme02N  41372  cdleme0ex1N  41373  cdleme0ex2N  41374  cdleme7aa  41392  cdleme7c  41395  cdleme7d  41396  cdleme7e  41397  cdleme7ga  41398  cdleme7  41399  cdleme8  41400  cdleme11a  41410  cdleme17c  41438  cdleme22gb  41444  cdlemeda  41448  cdleme20k  41469  cdleme21a  41475  cdleme21d  41480  cdleme22f2  41497  cdleme22g  41498  cdleme23a  41499  cdleme23b  41500  cdleme23c  41501  cdleme24  41502  cdleme28  41523  cdlemefrs32fva1  41551  cdlemefr32sn2aw  41554  cdlemefs32sn1aw  41564  cdleme41sn3a  41583  cdleme32fva  41587  cdleme32fva1  41588  cdleme35a  41598  cdleme35b  41600  cdleme35c  41601  cdleme35f  41604  cdleme39a  41615  cdleme42a  41621  cdleme42c  41622  cdleme42b  41628  cdleme42e  41629  cdleme42f  41630  cdleme42g  41631  cdleme42h  41632  cdleme43bN  41640  cdleme46f2g2  41643  cdleme17d2  41645  cdleme17d4  41647  cdleme48fv  41649  cdleme48fvg  41650  cdleme4gfv  41657  cdlemeg46c  41663  cdlemeg46nlpq  41667  cdlemeg46gfre  41682  cdleme48d  41685  cdlemeg49lebilem  41689  cdleme50trn2  41701  cdleme50ltrn  41707  cdleme  41710  cdlemf1  41711  cdlemf  41713  trlord  41719  ltrniotacnvval  41732  ltrniotavalbN  41734  cdlemg1cex  41738  cdlemg2dN  41740  cdlemg2ce  41742  cdlemg2fvlem  41744  cdlemg2idN  41746  cdlemg2kq  41752  cdlemg2l  41753  cdlemg2m  41754  cdlemg4b2  41760  cdlemg7fvN  41774  cdlemg8a  41777  cdlemg10bALTN  41786  cdlemg11aq  41788  cdlemg12d  41796  cdlemg13a  41801  cdlemg13  41802  cdlemg14f  41803  cdlemg14g  41804  cdlemg17a  41811  cdlemg17b  41812  cdlemg27a  41842  cdlemg31b0N  41844  cdlemg31a  41847  cdlemg31b  41848  cdlemg31c  41849  ltrnco  41869  trlcoabs  41871  trlcoabs2N  41872  trlcocnvat  41874  trlconid  41875  trlcolem  41876  trlcone  41878  cdlemg42  41879  cdlemg43  41880  cdlemg46  41885  cdlemg47  41886  tendoeq1  41914  tendoco2  41918  tendoplco2  41929  tendopltp  41930  cdlemh1  41965  cdlemh2  41966  cdlemi1  41968  cdlemi  41970  cdlemk1  41981  cdlemk2  41982  cdlemk3  41983  cdlemk4  41984  cdlemk8  41988  cdlemk9  41989  cdlemk9bN  41990  cdlemk31  42046  cdlemk32  42047  cdlemk28-3  42058  cdlemk19u  42120  cdlemk56w  42123  tendoex  42125  erngdvlem4  42141  erngdvlem4-rN  42149  dia11N  42198  dib11N  42310  cdlemn6  42352  cdlemn7  42353  cdlemn8  42354  cdlemn9  42355  dihordlem6  42363  dihordlem7  42364  dihord1  42368  dihord2a  42369  dihord2b  42370  dihord2pre  42375  dihord2pre2  42376  dihlsscpre  42384  dihvalcq2  42397  dihopelvalcpre  42398  dihord4  42408  dihord6b  42410  dihmeetlem1N  42440  dihglblem3N  42445  dihmeetlem2N  42449  dihglbcpreN  42450  dihmeetcN  42452  dihmeetbclemN  42454  dihmeetlem4preN  42456  dihjatc1  42461  dihjatc2N  42462  dihjatc3  42463  dihmeetlem9N  42465  dihmeetlem13N  42469  dihmeetlem20N  42476  dih1dimatlem0  42478  mapdpglem24  42854  mapdpglem32  42855  baerlem3lem2  42860  baerlem5alem2  42861  baerlem5blem2  42862  mapdh9aOLDN  42940  hdmap14lem6  43023  sn-addlid  43548  mzpsubst  43852  pellexlem5  43933  pellex  43935  pell14qrexpclnn0  43966  pellfundex  43986  qirropth  44008  monotuz  44041  congtr  44065  congmul  44067  congsub  44070  mzpcong  44072  fzmaxdif  44081  jm2.15nn0  44103  idomsubgmo  44288  iunrelexpmin1  44801  iunrelexpmin2  44805  trclimalb2  44819  mnringmulrcld  45319  fourierdlem42  47252  fourierdlem48  47257  fourierdlem80  47289  smfaddlem1  47866  prmdvdsfmtnof1lem1  48762  uhgrimisgrgric  49122  uspgropssxp  49335  lidldomn1  49421  rngccatidALTV  49462  coe1sclmulval  49590  lincdifsn  49629  seposep  50133  iscnrm3rlem8  50154  iscnrm3llem2  50157