Theorem simp2l 1197

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 1132	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp12l  1284  simp22l  1290  simp32l  1296  fsnunf  7188  f1oiso2  7354  fpr3g  8282  omeulem2  8595  uniinqs  8805  unxpdomlem3  9266  gruina  10827  dedekind  11393  addlid  11413  subaddmulsub  11693  dmdcan  11940  xaddass  13246  xaddass2  13247  xlt2add  13257  xmulasslem3  13283  xadddi2  13294  xadddi2r  13295  expaddzlem  14088  expaddz  14089  expmulz  14091  expdiv  14096  expmordi  14149  modexp  14218  pfxeq  14664  ccatopth2  14685  swrdco  14806  o1add  15576  o1mul  15577  o1sub  15578  fsumsplitsnun  15719  ntrivcvgmul  15866  prmexpb  16676  pcpremul  16797  pcdiv  16806  pcqmul  16807  pcqdiv  16811  4sqlem12  16910  f1ocpbllem  17491  ercpbl  17516  erlecpbl  17517  latjlej12  18432  latmlem12  18448  latj4  18466  latj4rot  18467  gsumsgrpccat  18777  gsmsymgreqlem2  19370  symgsssg  19406  symgfisg  19407  mndodcong  19481  cmn4  19740  ablsub4  19749  abladdsub4  19750  lsm4  19799  abvdom  20700  abvres  20701  abvtrivd  20702  lspsnvs  20984  lspsneu  20993  lspfixed  20998  lspexch  20999  lsmcv  21011  lspsolvlem  21012  ring2idlqus1  21191  coe1sclmulfv  22176  matvscacell  22312  m1detdiag  22473  cramerimplem3  22561  cnprest  23167  hausnei2  23231  isreg2  23255  cmpcld  23280  llyrest  23363  nllyrest  23364  elptr  23451  basqtop  23589  hausflimlem  23857  tmdgsum  23973  utop2nei  24129  trcfilu  24173  ssblps  24302  ssbl  24303  prdsxmslem2  24412  tgqioo  24690  metnrm  24752  bndth  24858  ncvspi  25058  ncvs1  25059  cph2ass  25115  lmmbr2  25161  iscau3  25180  bcthlem5  25230  ovolunlem2  25401  dvres2  25815  dvfsumlem2  25935  dvfsumlem2OLD  25936  plyadd  26125  plymul  26126  coeeu  26133  coemullem  26158  aalioulem4  26244  mulcxp  26593  cxplea  26604  cxple2  26605  cxplt2  26606  cxpcn3lem  26656  angcan  26708  ang180lem5  26719  divsqrtsumlem  26886  logexprlim  27132  dchrvmasumlema  27407  dchrisum0lema  27421  logdivsum  27440  log2sumbnd  27451  abvcxp  27522  padicabv  27537  nolesgn2ores  27579  nosupres  27614  nosupbnd1lem1  27615  nosupbnd1lem2  27616  nosupbnd1lem4  27618  nosupbnd1lem5  27619  nosupbnd1lem6  27620  noinffv  27628  noinfres  27629  noinfbnd1lem1  27630  noinfbnd1lem2  27631  noinfbnd1lem4  27633  noinfbnd1lem6  27635  nosupinfsep  27639  scutbdaylt  27725  tghilberti2  28416  brbtwn2  28690  axcontlem4  28752  axcontlem8  28756  clwlkl1loop  29571  clwwlknonex2lem2  29892  clwlknon2num  30152  numclwlk1lem2  30154  chscllem4  31424  orngmul  32945  measxun2  33752  measun  33753  mbfmco2  33808  probun  33962  satfv1fvfmla1  34956  cgrcomim  35508  cgrcoml  35515  cgrcomr  35516  cgrdegen  35523  btwnintr  35538  btwnexch3  35539  btwnouttr2  35541  btwnouttr  35543  btwnexch  35544  btwndiff  35546  lineid  35602  idinside  35603  btwnconn1lem7  35612  btwnconn1lem8  35613  btwnconn1lem9  35614  btwnconn1lem12  35617  btwnconn1lem14  35619  btwnconn3  35622  midofsegid  35623  segcon2  35624  brsegle2  35628  btwnoutside  35644  outsideoftr  35648  outsideofeu  35650  linethru  35672  cnres2  37158  heibor  37216  lsmsat  38404  lkrlsp  38498  lkrlsp2  38499  lkrlsp3  38500  latm4  38629  omlspjN  38657  hlatj4  38770  4noncolr3  38850  4noncolr2  38851  4noncolr1  38852  athgt  38853  3dimlem3a  38857  3dimlem4a  38860  3dimlem4  38861  3dimlem4OLDN  38862  3dim3  38866  1cvratex  38870  hlatexch4  38878  3atlem4  38883  atcvrlln2  38916  atcvrlln  38917  lplnnlelln  38940  lvoli2  38978  lvolnlelln  38981  lvolnlelpln  38982  4atlem11b  39005  4atlem12b  39008  2lplnja  39016  2lplnj  39017  dalemyeo  39029  dath2  39134  lncvrat  39179  cdlemblem  39190  cdlemb  39191  elpaddri  39199  padd4N  39237  llnmod2i2  39260  llnexchb2  39266  dalawlem1  39268  dalawlem2  39269  pclfinN  39297  osumcllem6N  39358  pexmidlem3N  39369  lhp2lt  39398  lhp2at0  39429  lhp2atnle  39430  lhp2atne  39431  lhp2at0nle  39432  lhp2at0ne  39433  lhpelim  39434  lhpmod2i2  39435  lhpmod6i1  39436  lhple  39439  lhpat  39440  lhpat3  39443  ltrncoelN  39540  ltrncoat  39541  ltrncnv  39543  trlat  39566  trl0  39567  ltrnnidn  39571  trlnid  39576  cdlemd7  39601  cdleme0b  39609  cdleme0c  39610  cdleme0fN  39615  cdleme02N  39619  cdleme0ex1N  39620  cdleme0ex2N  39621  cdleme7aa  39639  cdleme7c  39642  cdleme7d  39643  cdleme7e  39644  cdleme7ga  39645  cdleme7  39646  cdleme8  39647  cdleme11a  39657  cdleme17c  39685  cdleme22gb  39691  cdlemeda  39695  cdleme20k  39716  cdleme21a  39722  cdleme21d  39727  cdleme22f2  39744  cdleme22g  39745  cdleme23a  39746  cdleme23b  39747  cdleme23c  39748  cdleme24  39749  cdleme28  39770  cdlemefrs32fva1  39798  cdlemefr32sn2aw  39801  cdlemefs32sn1aw  39811  cdleme41sn3a  39830  cdleme32fva  39834  cdleme32fva1  39835  cdleme35a  39845  cdleme35b  39847  cdleme35c  39848  cdleme35f  39851  cdleme39a  39862  cdleme42a  39868  cdleme42c  39869  cdleme42b  39875  cdleme42e  39876  cdleme42f  39877  cdleme42g  39878  cdleme42h  39879  cdleme43bN  39887  cdleme46f2g2  39890  cdleme17d2  39892  cdleme17d4  39894  cdleme48fv  39896  cdleme48fvg  39897  cdleme4gfv  39904  cdlemeg46c  39910  cdlemeg46nlpq  39914  cdlemeg46gfre  39929  cdleme48d  39932  cdlemeg49lebilem  39936  cdleme50trn2  39948  cdleme50ltrn  39954  cdleme  39957  cdlemf1  39958  cdlemf  39960  trlord  39966  ltrniotacnvval  39979  ltrniotavalbN  39981  cdlemg1cex  39985  cdlemg2dN  39987  cdlemg2ce  39989  cdlemg2fvlem  39991  cdlemg2idN  39993  cdlemg2kq  39999  cdlemg2l  40000  cdlemg2m  40001  cdlemg4b2  40007  cdlemg7fvN  40021  cdlemg8a  40024  cdlemg10bALTN  40033  cdlemg11aq  40035  cdlemg12d  40043  cdlemg13a  40048  cdlemg13  40049  cdlemg14f  40050  cdlemg14g  40051  cdlemg17a  40058  cdlemg17b  40059  cdlemg27a  40089  cdlemg31b0N  40091  cdlemg31a  40094  cdlemg31b  40095  cdlemg31c  40096  ltrnco  40116  trlcoabs  40118  trlcoabs2N  40119  trlcocnvat  40121  trlconid  40122  trlcolem  40123  trlcone  40125  cdlemg42  40126  cdlemg43  40127  cdlemg46  40132  cdlemg47  40133  tendoeq1  40161  tendoco2  40165  tendoplco2  40176  tendopltp  40177  cdlemh1  40212  cdlemh2  40213  cdlemi1  40215  cdlemi  40217  cdlemk1  40228  cdlemk2  40229  cdlemk3  40230  cdlemk4  40231  cdlemk8  40235  cdlemk9  40236  cdlemk9bN  40237  cdlemk31  40293  cdlemk32  40294  cdlemk28-3  40305  cdlemk19u  40367  cdlemk56w  40370  tendoex  40372  erngdvlem4  40388  erngdvlem4-rN  40396  dia11N  40445  dib11N  40557  cdlemn6  40599  cdlemn7  40600  cdlemn8  40601  cdlemn9  40602  dihordlem6  40610  dihordlem7  40611  dihord1  40615  dihord2a  40616  dihord2b  40617  dihord2pre  40622  dihord2pre2  40623  dihlsscpre  40631  dihvalcq2  40644  dihopelvalcpre  40645  dihord4  40655  dihord6b  40657  dihmeetlem1N  40687  dihglblem3N  40692  dihmeetlem2N  40696  dihglbcpreN  40697  dihmeetcN  40699  dihmeetbclemN  40701  dihmeetlem4preN  40703  dihjatc1  40708  dihjatc2N  40709  dihjatc3  40710  dihmeetlem9N  40712  dihmeetlem13N  40716  dihmeetlem20N  40723  dih1dimatlem0  40725  mapdpglem24  41101  mapdpglem32  41102  baerlem3lem2  41107  baerlem5alem2  41108  baerlem5blem2  41109  mapdh9aOLDN  41187  hdmap14lem6  41270  nnadddir  41757  sn-addlid  41871  mzpsubst  42080  pellexlem5  42165  pellex  42167  pell14qrexpclnn0  42198  pellfundex  42218  qirropth  42240  monotuz  42274  congtr  42298  congmul  42300  congsub  42303  mzpcong  42305  fzmaxdif  42314  jm2.15nn0  42336  idomsubgmo  42533  iunrelexpmin1  43051  iunrelexpmin2  43055  trclimalb2  43069  mnringmulrcld  43578  fourierdlem42  45450  fourierdlem48  45455  fourierdlem80  45487  smfaddlem1  46064  prmdvdsfmtnof1lem1  46837  uspgropssxp  47119  lidldomn1  47206  rngccatidALTV  47247  coe1sclmulval  47366  lincdifsn  47405  seposep  47857  iscnrm3rlem8  47879  iscnrm3llem2  47882